begin	comment Axioma#s van Heyting;
	integer en, of, niet, Stelling En12, Stelling En1, Stelling En2, Stelling En21, Stelling Of1, Stelling VV;
	integer procedure En (a, b); integer a, b; En:= form2 (en, a, b);
	integer procedure Of (a, b); integer a, b; Of:= form2 (of, a, b);
	integer procedure Niet (a); integer a; Niet:= form1 (niet, a);

	integer procedure En12 (p, q); value p, q; integer p, q;
	comment Gegeven p en q, bewijs p & q;
	En12:= Concl (q, Concl (p, Subst (q, Subst (p, Stelling En12))));

	integer procedure En1 (p, q); value p, q; integer p, q;
	comment Gegeven p & q, bewijs p;
	En1:= Concl (En (p, q), Subst (q, Subst (p, Stelling En1)));

	integer procedure En2 (p, q); value p, q; integer p, q;
	comment Gegeven p & q, bewijs q;
	En2:= Concl (En (p, q), Subst (q, Subst (p, Stelling En2)));

	integer procedure En21 (p, q); value p, q; integer p, q;
	comment Gegeven p & q, bewijs q & p;
	En21:= Concl (En (p, q), Subst (q, Subst (p, Stelling En21)));

	integer procedure Ververs (p); value p; integer p;
	comment Gegeven p, bewijs p;
	Ververs:= Concl (p, Subst (p, Stelling VV));

	integer procedure Of1 (p, q); value p, q; integer p, q;
	comment Gegeven p, bewijs p | q;
	Of1:= Concl (p, Subst (q, Subst (p, Stelling Of1)));

	integer procedure Terug1 (a); value a; integer a;
	comment Wanneer Terug1 i.p.v. Terug wordt aangeroepen, wordt de te binden variabele vervangen door a;
	begin	integer F;
		F:= Terug; Intro (a); Subst (a, F); Terug1:= Terug
	end;

	BEGIN;
	Definieer (en, 080, En (a, b), A (z, Impl (Impl (a, Impl (b, z)), z)));
	Definieer (of, 079, Of (a, b), A (y, Impl (En (Impl (a, y), Impl (b, y)), y)));
	Definieer (niet, 076, Niet (a), A (x, Impl (a, x)));

	comment Hulpstellingen;
	Intro (c); Stel (c); Terug; Stelling VV:= Terug;
	Intro (d); Intro (e); Stel (d); Stel (e); Intro (z);
	Concl (e, Concl (d, Stel (Impl (d, Impl (e, z)))));
	Terug; Terug; DefRL (En (d, e)); Terug; Terug; Terug; Stelling En12:= Terug;
	Intro (f); Intro (g); Stel (En (f, g));
	Stel (f); Stel (g); Ververs (f); Terug; Concl (Terug, Subst (f, DefLR (En (f, g))));
	Terug; Terug; Stelling En1:= Terug;
	Intro (h); Intro (i); Stel (En (h, i));
	Stel (h); Stel (i); Terug; Concl (Terug, Subst (i, DefLR (En (h, i))));
	Terug; Terug; Stelling En2:= Terug;
	Intro (j); Intro (k); Stel (En (j, k));
	En12 (En2 (j, k), En1 (j, k));
	Terug; Terug; Stelling En21:= Terug;
	Intro (l); Intro (m); Stel (l);
	Intro (y); Stel (En (Impl (l, y), Impl (m, y))); Concl (l, En1 (Impl (l, y), Impl (m, y)));
	Terug; Terug; DefRL (Of (l, m)); Terug; Terug; Stelling Of1:= Terug;

I:	Intro (p);
	Stel (p);
	En12 (p, p); QED;

II:	Intro (p); Intro (q);
	Stel (En (p, q));
	En21 (p, q); QED;

III:	Intro (p); Intro (q); Intro (r);
	F[1]:= Impl (p, q); Stel (F[1]);
	Stel (En (p, r));
	En1 (p, r);
	Concl (p, F[1]);
	En2 (p, r);
	En12 (q, r); QED;

IV:	Intro (p); Intro (q); Intro (r);
	F[1]:= Impl (p, q); F[2]:= Impl (q, r);
	Stel (En (F[1], F[2]));
	Stel (p);
	En1 (F[1], F[2]);
	Concl (p, F[1]);
	En2 (F[1], F[2]);
	Concl (q, F[2]); QED;

V:	Intro (p); Intro (q);
	Stel (q); Stel (p); Ververs (q); QED;

VI:	Intro (p); Intro (q);
	F[1]:= Impl (p, q);
	Stel (En (p, F[1]));
	En1 (p, F[1]);
	En2 (p, F[1]);
	Concl (p, F[1]); QED;

VII:	Intro (p); Intro (q);
	Stel (p); Of1 (p, q); QED;

VIII:	Intro (p); Intro (q);
	Stel (Of (p, q));
	Intro (w);
	F[1]:= Impl (p, w); F[2]:= Impl (q, w);
	Stel (En (F[2], F[1]));
	F[3]:= En21 (F[2], F[1]);
	F[4]:= DefLR (Of (p, q));
	F[5]:= Subst (w, F[4]);
	Concl (F[3], F[5]);
	Terug;
	Terug1 (y);
	DefRL (Of (p, q)); QED;

IX:	Intro (p); Intro (q); Intro (r);
	F[1]:= En (Impl (p, r), Impl (q, r)); Stel (F[1]);
	F[2]:= Of (p, q); Stel (F[2]);
	F[3]:= DefLR (F[2]);
	F[4]:= Subst (r, F[3]);
	Concl (F[1], F[4]); QED;

X:	Intro (p); Intro (q);
	F[1]:= Niet (p); Stel (F[1]);
	Subst (q, DefLR (F[1])); QED;

XI:	Intro (p); Intro (q); Intro (r);
	F[1]:= Impl (p, q);
	F[2]:= Impl (p, Niet (q));
	Stel (En (F[1], F[2]));
	Intro (w);
	Stel (p);
	F[3]:= En1 (F[1], F[2]);
	Concl (p, F[3]);
	F[4]:= En2 (F[1], F[2]);
	Concl (p, F[4]);
	F[5]:= DefLR (Niet (q));
	F[6]:= Subst (w, F[5]);
	Concl (q, F[6]);
	Terug;
	Terug1 (x);
	DefRL (Niet (p)); QED
end