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