let SAS be AffinPlane; ( SAS is Desarguesian implies for o, a, a', b, b', c, c' being Element of st not o,a // o,b & not o,a // o,c & o,a // o,a' & o,b // o,b' & o,c // o,c' & a,b // a',b' & a,c // a',c' holds
b,c // b',c' )
assume A1:
SAS is Desarguesian
; for o, a, a', b, b', c, c' being Element of st not o,a // o,b & not o,a // o,c & o,a // o,a' & o,b // o,b' & o,c // o,c' & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
let o, a, a', b, b', c, c' be Element of ; ( not o,a // o,b & not o,a // o,c & o,a // o,a' & o,b // o,b' & o,c // o,c' & a,b // a',b' & a,c // a',c' implies b,c // b',c' )
assume that
A2:
not o,a // o,b
and
A3:
not o,a // o,c
and
A4:
o,a // o,a'
and
A5:
o,b // o,b'
and
A6:
o,c // o,c'
and
A7:
( a,b // a',b' & a,c // a',c' )
; b,c // b',c'
A8:
( o <> a & o <> b )
by A2, AFF_1:12;
A9:
o <> c
by A3, AFF_1:12;
LIN o,b,b'
by A5, AFF_1:def 1;
then consider P being Subset of such that
A10:
( P is being_line & o in P )
and
A11:
b in P
and
A12:
b' in P
by AFF_1:33;
LIN o,a,a'
by A4, AFF_1:def 1;
then consider A being Subset of such that
A13:
( A is being_line & o in A & a in A )
and
A14:
a' in A
by AFF_1:33;
LIN o,c,c'
by A6, AFF_1:def 1;
then consider C being Subset of such that
A15:
( C is being_line & o in C )
and
A16:
c in C
and
A17:
c' in C
by AFF_1:33;
A18:
A <> C
by A3, A13, A16, AFF_1:65;
A <> P
by A2, A13, A11, AFF_1:65;
hence
b,c // b',c'
by A1, A7, A13, A14, A10, A11, A12, A15, A16, A17, A8, A9, A18, AFF_2:def 4; verum