# 230267 -     94 #


(a & b) is gedefinieerd als A z: ((a => (b => z)) => z)

(a | b) is gedefinieerd als A y: (((a => y) & (b => y)) => y)

! a is gedefinieerd als A x: (a => x)

	Zij c een uitspraak
		Stel c
	(c => c)
A c: (c => c)
	Zij d een uitspraak
		Zij e een uitspraak
			Stel d
				Stel e
					Zij z een uitspraak
						Stel (d => (e => z))
						d
						Dus (e => z)
						e
						Dus z
					((d => (e => z)) => z)
				A z: ((d => (e => z)) => z)
			[&]	(d & e)
			(e => (d & e))
		(d => (e => (d & e)))
	A e: (d => (e => (d & e)))
A d: A e: (d => (e => (d & e)))
	Zij f een uitspraak
		Zij g een uitspraak
			Stel (f & g)
				Stel f
					Stel g

					A c: (c => c)
					substitutie van f voor c
					(f => f)
					f
					Dus f
				(g => f)
			(f => (g => f))

			(f & g)
		[&]	A z: ((f => (g => z)) => z)
			substitutie van f voor z
			((f => (g => f)) => f)
			(f => (g => f))
			Dus f
		((f & g) => f)
	A g: ((f & g) => f)
A f: A g: ((f & g) => f)
	Zij h een uitspraak
		Zij i een uitspraak
			Stel (h & i)
				Stel h
					Stel i
				(i => i)
			(h => (i => i))

			(h & i)
		[&]	A z: ((h => (i => z)) => z)
			substitutie van i voor z
			((h => (i => i)) => i)
			(h => (i => i))
			Dus i
		((h & i) => i)
	A i: ((h & i) => i)
A h: A i: ((h & i) => i)
	Zij j een uitspraak
		Zij k een uitspraak
			Stel (j & k)

			A h: A i: ((h & i) => i)
			substitutie van j voor h
			A i: ((j & i) => i)
			substitutie van k voor i
			((j & k) => k)
			(j & k)
			Dus k

			A f: A g: ((f & g) => f)
			substitutie van j voor f
			A g: ((j & g) => j)
			substitutie van k voor g
			((j & k) => j)
			(j & k)
			Dus j

			A d: A e: (d => (e => (d & e)))
			substitutie van k voor d
			A e: (k => (e => (k & e)))
			substitutie van j voor e
			(k => (j => (k & j)))
			k
			Dus (j => (k & j))
			j
			Dus (k & j)
		((j & k) => (k & j))
	A k: ((j & k) => (k & j))
A j: A k: ((j & k) => (k & j))
	Zij l een uitspraak
		Zij m een uitspraak
			Stel l
				Zij y een uitspraak
					Stel ((l => y) & (m => y))

					A f: A g: ((f & g) => f)
					substitutie van (l => y) voor f
					A g: (((l => y) & g) => (l => y))
					substitutie van (m => y) voor g
					(((l => y) & (m => y)) => (l => y))
					((l => y) & (m => y))
					Dus (l => y)
					l
					Dus y
				(((l => y) & (m => y)) => y)
			A y: (((l => y) & (m => y)) => y)
		[|]	(l | m)
		(l => (l | m))
	A m: (l => (l | m))
A l: A m: (l => (l | m))
	Zij p een uitspraak
		Stel p

		A d: A e: (d => (e => (d & e)))
		substitutie van p voor d
		A e: (p => (e => (p & e)))
		substitutie van p voor e
		(p => (p => (p & p)))
		p
		Dus (p => (p & p))
		p
		Dus (p & p)
	(p => (p & p))
A p: (p => (p & p))
Q.E.D.

	Zij p een uitspraak
		Zij q een uitspraak

		A j: A k: ((j & k) => (k & j))
		substitutie van p voor j
		A k: ((p & k) => (k & p))
		substitutie van q voor k
		((p & q) => (q & p))
	A q: ((p & q) => (q & p))
A p: A q: ((p & q) => (q & p))
Q.E.D.

	Zij p een uitspraak
		Zij q een uitspraak
			Zij r een uitspraak
				Stel (p => q)
					Stel (p & r)

					A f: A g: ((f & g) => f)
					substitutie van p voor f
					A g: ((p & g) => p)
					substitutie van r voor g
					((p & r) => p)
					(p & r)
					Dus p

					(p => q)
					p
					Dus q

					A h: A i: ((h & i) => i)
					substitutie van p voor h
					A i: ((p & i) => i)
					substitutie van r voor i
					((p & r) => r)
					(p & r)
					Dus r

					A d: A e: (d => (e => (d & e)))
					substitutie van q voor d
					A e: (q => (e => (q & e)))
					substitutie van r voor e
					(q => (r => (q & r)))
					q
					Dus (r => (q & r))
					r
					Dus (q & r)
				((p & r) => (q & r))
			((p => q) => ((p & r) => (q & r)))
		A r: ((p => q) => ((p & r) => (q & r)))
	A q: A r: ((p => q) => ((p & r) => (q & r)))
A p: A q: A r: ((p => q) => ((p & r) => (q & r)))
Q.E.D.

	Zij p een uitspraak
		Zij q een uitspraak
			Zij r een uitspraak
				Stel ((p => q) & (q => r))
					Stel p

					A f: A g: ((f & g) => f)
					substitutie van (p => q) voor f
					A g: (((p => q) & g) => (p => q))
					substitutie van (q => r) voor g
					(((p => q) & (q => r)) => (p => q))
					((p => q) & (q => r))
					Dus (p => q)
					p
					Dus q

					A h: A i: ((h & i) => i)
					substitutie van (p => q) voor h
					A i: (((p => q) & i) => i)
					substitutie van (q => r) voor i
					(((p => q) & (q => r)) => (q => r))
					((p => q) & (q => r))
					Dus (q => r)
					q
					Dus r
				(p => r)
			(((p => q) & (q => r)) => (p => r))
		A r: (((p => q) & (q => r)) => (p => r))
	A q: A r: (((p => q) & (q => r)) => (p => r))
A p: A q: A r: (((p => q) & (q => r)) => (p => r))
Q.E.D.

	Zij p een uitspraak
		Zij q een uitspraak
			Stel q
				Stel p

				A c: (c => c)
				substitutie van q voor c
				(q => q)
				q
				Dus q
			(p => q)
		(q => (p => q))
	A q: (q => (p => q))
A p: A q: (q => (p => q))
Q.E.D.

	Zij p een uitspraak
		Zij q een uitspraak
			Stel (p & (p => q))

			A f: A g: ((f & g) => f)
			substitutie van p voor f
			A g: ((p & g) => p)
			substitutie van (p => q) voor g
			((p & (p => q)) => p)
			(p & (p => q))
			Dus p

			A h: A i: ((h & i) => i)
			substitutie van p voor h
			A i: ((p & i) => i)
			substitutie van (p => q) voor i
			((p & (p => q)) => (p => q))
			(p & (p => q))
			Dus (p => q)
			p
			Dus q
		((p & (p => q)) => q)
	A q: ((p & (p => q)) => q)
A p: A q: ((p & (p => q)) => q)
Q.E.D.

	Zij p een uitspraak
		Zij q een uitspraak

		A l: A m: (l => (l | m))
		substitutie van p voor l
		A m: (p => (p | m))
		substitutie van q voor m
		(p => (p | q))
	A q: (p => (p | q))
A p: A q: (p => (p | q))
Q.E.D.

	Zij p een uitspraak
		Zij q een u77