let SAS be AffinPlane; :: thesis: ( SAS is translational implies for a, a9, b, b9, c, c9 being Element of SAS st not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9 )
assume A1: SAS is translational ; :: thesis: for a, a9, b, b9, c, c9 being Element of SAS st not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
let a, a9, b, b9, c, c9 be Element of SAS; :: thesis: ( not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )
assume that
A2: not a,a9 // a,b and
A3: not a,a9 // a,c and
A4: a,a9 // b,b9 and
A5: a,a9 // c,c9 and
A6: ( a,b // a9,b9 & a,c // a9,c9 ) ; :: thesis: b,c // b9,c9
set A = Line (a,a9);
A7: a <> a9 by A2, AFF_1:3;
then A8: Line (a,a9) is being_line by AFF_1:def 3;
then consider C being Subset of SAS such that
A9: c in C and
A10: Line (a,a9) // C by AFF_1:49;
A11: C is being_line by A10, AFF_1:36;
A12: ( a in Line (a,a9) & a9 in Line (a,a9) ) by AFF_1:15;
then A13: Line (a,a9) <> C by A3, A8, A9, AFF_1:51;
A14: a,a9 // Line (a,a9) by A8, A12, AFF_1:23;
then a,a9 // C by A10, AFF_1:43;
then c,c9 // C by A5, A7, AFF_1:32;
then A15: c9 in C by A9, A11, AFF_1:23;
consider P being Subset of SAS such that
A16: b in P and
A17: Line (a,a9) // P by A8, AFF_1:49;
A18: P is being_line by A17, AFF_1:36;
a,a9 // P by A14, A17, AFF_1:43;
then b,b9 // P by A4, A7, AFF_1:32;
then A19: b9 in P by A16, A18, AFF_1:23;
Line (a,a9) <> P by A2, A8, A12, A16, AFF_1:51;
hence b,c // b9,c9 by A1, A6, A8, A12, A16, A17, A9, A10, A18, A11, A19, A15, A13, AFF_2:def 11; :: thesis: verum