let SAS be Semi_Affine_Space; :: thesis: for a, b being Element of SAS st a <> b holds
ex c being Element of SAS st
( a,b,c are_collinear & c <> a & c <> b )
let a, b be Element of SAS; :: thesis: ( a <> b implies ex c being Element of SAS st
( a,b,c are_collinear & c <> a & c <> b ) )
assume a <> b ; :: thesis: ex c being Element of SAS st
( a,b,c are_collinear & c <> a & c <> b )
then consider p being Element of SAS such that
A1: not a,b,p are_collinear by Th25;
consider q being Element of SAS such that
A2: parallelogram a,b,p,q by A1, Th44;
not p,q,b are_collinear by A2, Th38;
then consider c being Element of SAS such that
A3: parallelogram p,q,b,c by Th44;
take c ; :: thesis: ( a,b,c are_collinear & c <> a & c <> b )
A4: p,q // b,c by A3;
( p <> q & a,b // p,q ) by A2, Th36;
then a,b // b,c by A4, Th8;
then b,a // b,c by Th6;
then A5: b,a,c are_collinear ;
A6: not a,q // b,p by A2, Th46;
( p,b // q,c & not b,c,p are_collinear ) by A3, Th37;
hence ( a,b,c are_collinear & c <> a & c <> b ) by A6, A5, Th6, Th22, Th24; :: thesis: verum