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 & parallelogram a,b,p,q ) 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 & a,b // p,q & p,q // b,c & p,b // q,c ) by A2, A3, Def3, Th54;
A5: not b,c,p is_collinear by A3, Th55;
a,b // b,c by A4, Th20;
then ( b,a // b,c & not a,q // b,p & c,q // b,p ) by A2, A4, Th17, Th64;
then ( b,a,c is_collinear & a <> c ) by Def2;
hence ( a,b,c is_collinear & c <> a & c <> b ) by A5, Th37, Th40; :: thesis: verum