let AFP be AffinPlane; ( AFP is Desarguesian iff for o, a, a', p, p', q, q' being Element of st LIN o,a,a' & LIN o,p,p' & LIN o,q,q' & not LIN o,a,p & not LIN o,a,q & a,p // a',p' & a,q // a',q' holds
p,q // p',q' )
thus
( AFP is Desarguesian implies for o, a, a', p, p', q, q' being Element of st LIN o,a,a' & LIN o,p,p' & LIN o,q,q' & not LIN o,a,p & not LIN o,a,q & a,p // a',p' & a,q // a',q' holds
p,q // p',q' )
( ( for o, a, a', p, p', q, q' being Element of st LIN o,a,a' & LIN o,p,p' & LIN o,q,q' & not LIN o,a,p & not LIN o,a,q & a,p // a',p' & a,q // a',q' holds
p,q // p',q' ) implies AFP is Desarguesian )proof
assume A1:
AFP is
Desarguesian
;
for o, a, a', p, p', q, q' being Element of st LIN o,a,a' & LIN o,p,p' & LIN o,q,q' & not LIN o,a,p & not LIN o,a,q & a,p // a',p' & a,q // a',q' holds
p,q // p',q'
let o,
a,
a',
p,
p',
q,
q' be
Element of ;
( LIN o,a,a' & LIN o,p,p' & LIN o,q,q' & not LIN o,a,p & not LIN o,a,q & a,p // a',p' & a,q // a',q' implies p,q // p',q' )
assume that A2:
LIN o,
a,
a'
and A3:
LIN o,
p,
p'
and A4:
LIN o,
q,
q'
and A5:
not
LIN o,
a,
p
and A6:
not
LIN o,
a,
q
and A7:
a,
p // a',
p'
and A8:
a,
q // a',
q'
;
p,q // p',q'
set A =
Line o,
a;
set P =
Line o,
p;
set C =
Line o,
q;
A9:
a in Line o,
a
by AFF_1:26;
A10:
o <> a
by A5, AFF_1:16;
then A11:
Line o,
a is
being_line
by AFF_1:def 3;
A12:
o in Line o,
a
by AFF_1:26;
then A13:
a' in Line o,
a
by A2, A10, A11, A9, AFF_1:39;
A14:
q in Line o,
q
by AFF_1:26;
then A15:
Line o,
a <> Line o,
q
by A6, A11, A12, A9, AFF_1:33;
A16:
o in Line o,
p
by AFF_1:26;
A17:
p in Line o,
p
by AFF_1:26;
A18:
o <> p
by A5, AFF_1:16;
then A19:
Line o,
p is
being_line
by AFF_1:def 3;
then A20:
p' in Line o,
p
by A3, A18, A16, A17, AFF_1:39;
A21:
o in Line o,
q
by AFF_1:26;
A22:
o <> q
by A6, AFF_1:16;
then A23:
Line o,
q is
being_line
by AFF_1:def 3;
then A24:
q' in Line o,
q
by A4, A22, A21, A14, AFF_1:39;
Line o,
a <> Line o,
p
by A5, A11, A12, A9, A17, AFF_1:33;
hence
p,
q // p',
q'
by A1, A7, A8, A10, A18, A22, A11, A19, A23, A12, A9, A16, A17, A21, A14, A13, A20, A24, A15, AFF_2:def 4;
verum
end;
assume A25:
for o, a, a', p, p', q, q' being Element of st LIN o,a,a' & LIN o,p,p' & LIN o,q,q' & not LIN o,a,p & not LIN o,a,q & a,p // a',p' & a,q // a',q' holds
p,q // p',q'
; AFP is Desarguesian
now let A,
P,
C be
Subset of ;
for o, a, b, c, a', b', c' being Element of st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'let o,
a,
b,
c,
a',
b',
c' be
Element of ;
( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' implies b,c // b',c' )assume that A26:
o in A
and A27:
o in P
and A28:
o in C
and A29:
o <> a
and A30:
o <> b
and A31:
o <> c
and A32:
a in A
and A33:
a' in A
and A34:
b in P
and A35:
b' in P
and A36:
c in C
and A37:
c' in C
and A38:
A is
being_line
and A39:
P is
being_line
and A40:
C is
being_line
and A41:
A <> P
and A42:
A <> C
and A43:
a,
b // a',
b'
and A44:
a,
c // a',
c'
;
b,c // b',c'A45:
LIN o,
b,
b'
by A27, A34, A35, A39, AFF_1:33;
A46:
not
LIN o,
a,
c
proof
assume
LIN o,
a,
c
;
contradiction
then
c in A
by A26, A29, A32, A38, AFF_1:39;
hence
contradiction
by A26, A28, A31, A36, A38, A40, A42, AFF_1:30;
verum
end; A47:
not
LIN o,
a,
b
proof
assume
LIN o,
a,
b
;
contradiction
then
b in A
by A26, A29, A32, A38, AFF_1:39;
hence
contradiction
by A26, A27, A30, A34, A38, A39, A41, AFF_1:30;
verum
end; A48:
LIN o,
c,
c'
by A28, A36, A37, A40, AFF_1:33;
LIN o,
a,
a'
by A26, A32, A33, A38, AFF_1:33;
hence
b,
c // b',
c'
by A25, A43, A44, A45, A48, A47, A46;
verum end;
hence
AFP is Desarguesian
by AFF_2:def 4; verum