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 is_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 is_collinear & c <> a & c <> b ) )
assume a <> b ; :: thesis: ex c being Element of SAS st
( a,b,c is_collinear & c <> a & c <> b )
then consider p being Element of SAS such that
A1: not a,b,p is_collinear by Th41;
consider q being Element of SAS such that
A2: parallelogram a,b,p,q by A1, Th62;
not p,q,b is_collinear by A2, Th56;
then consider c being Element of SAS such that
A3: parallelogram p,q,b,c by Th62;
take c ; :: thesis: ( a,b,c is_collinear & c <> a & c <> b )
A4: p,q // b,c by A3, Def3;
( p <> q & a,b // p,q ) by A2, Def3, Th54;
then a,b // b,c by A4, Th20;
then b,a // b,c by Th17;
then A5: b,a,c is_collinear by Def2;
A6: not a,q // b,p by A2, Th64;
( p,b // q,c & not b,c,p is_collinear ) by A3, Def3, Th55;
hence ( a,b,c is_collinear & c <> a & c <> b ) by A6, A5, Th17, Th37, Th40; :: thesis: verum