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