let SAS be AffinPlane; :: thesis: ( SAS is translational implies for a, a', b, b', c, c' being Element of st not a,a' // a,b & not a,a' // a,c & a,a' // b,b' & a,a' // c,c' & a,b // a',b' & a,c // a',c' holds
b,c // b',c' )
assume A1: SAS is translational ; :: thesis: for a, a', b, b', c, c' being Element of st not a,a' // a,b & not a,a' // a,c & a,a' // b,b' & a,a' // c,c' & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
let a, a', b, b', c, c' be Element of ; :: thesis: ( not a,a' // a,b & not a,a' // a,c & a,a' // b,b' & a,a' // c,c' & a,b // a',b' & a,c // a',c' implies b,c // b',c' )
assume that
A2: not a,a' // a,b and
A3: not a,a' // a,c and
A4: a,a' // b,b' and
A5: a,a' // c,c' and
A6: ( a,b // a',b' & a,c // a',c' ) ; :: thesis: b,c // b',c'
set A = Line a,a';
A7: a <> a' by A2, AFF_1:12;
then A8: Line a,a' is being_line by AFF_1:def 3;
then consider C being Subset of such that
A9: c in C and
A10: Line a,a' // C by AFF_1:63;
A11: C is being_line by A10, AFF_1:50;
A12: ( a in Line a,a' & a' in Line a,a' ) by AFF_1:26;
then A13: Line a,a' <> C by A3, A8, A9, AFF_1:65;
A14: a,a' // Line a,a' by A8, A12, AFF_1:37;
then a,a' // C by A10, AFF_1:57;
then c,c' // C by A5, A7, AFF_1:46;
then A15: c' in C by A9, A11, AFF_1:37;
consider P being Subset of such that
A16: b in P and
A17: Line a,a' // P by A8, AFF_1:63;
A18: P is being_line by A17, AFF_1:50;
a,a' // P by A14, A17, AFF_1:57;
then b,b' // P by A4, A7, AFF_1:46;
then A19: b' in P by A16, A18, AFF_1:37;
Line a,a' <> P by A2, A8, A12, A16, AFF_1:65;
hence b,c // b',c' by A1, A6, A8, A12, A16, A17, A9, A10, A18, A11, A19, A15, A13, AFF_2:def 11; :: thesis: verum