let AFP be AffinPlane; ( AFP is Desarguesian iff for o, a, a9, p, p9, q, q9 being Element of AFP st LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 holds
p,q // p9,q9 )
thus
( AFP is Desarguesian implies for o, a, a9, p, p9, q, q9 being Element of AFP st LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 holds
p,q // p9,q9 )
( ( for o, a, a9, p, p9, q, q9 being Element of AFP st LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 holds
p,q // p9,q9 ) implies AFP is Desarguesian )proof
assume A1:
AFP is
Desarguesian
;
for o, a, a9, p, p9, q, q9 being Element of AFP st LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 holds
p,q // p9,q9
let o,
a,
a9,
p,
p9,
q,
q9 be
Element of
AFP;
( LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 implies p,q // p9,q9 )
assume that A2:
LIN o,
a,
a9
and A3:
LIN o,
p,
p9
and A4:
LIN o,
q,
q9
and A5:
not
LIN o,
a,
p
and A6:
not
LIN o,
a,
q
and A7:
a,
p // a9,
p9
and A8:
a,
q // a9,
q9
;
p,q // p9,q9
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:
a9 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:
p9 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:
q9 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 // p9,
q9
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, a9, p, p9, q, q9 being Element of AFP st LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 holds
p,q // p9,q9
; AFP is Desarguesian
now let A,
P,
C be
Subset of
AFP;
for o, a, b, c, a9, b9, c9 being Element of AFP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9let o,
a,
b,
c,
a9,
b9,
c9 be
Element of
AFP;
( o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )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:
a9 in A
and A34:
b in P
and A35:
b9 in P
and A36:
c in C
and A37:
c9 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 // a9,
b9
and A44:
a,
c // a9,
c9
;
b,c // b9,c9A45:
LIN o,
b,
b9
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,
c9
by A28, A36, A37, A40, AFF_1:33;
LIN o,
a,
a9
by A26, A32, A33, A38, AFF_1:33;
hence
b,
c // b9,
c9
by A25, A43, A44, A45, A48, A47, A46;
verum end;
hence
AFP is Desarguesian
by AFF_2:def 4; verum