let FdSp be FanodesSp; :: thesis: for a, b being Element of FdSp st a <> b holds
ex c being Element of FdSp st
( a,b,c are_collinear & c <> a & c <> b )
let a, b be Element of FdSp; :: thesis: ( a <> b implies ex c being Element of FdSp st
( a,b,c are_collinear & c <> a & c <> b ) )
assume a <> b ; :: thesis: ex c being Element of FdSp st
( a,b,c are_collinear & c <> a & c <> b )
then consider p being Element of FdSp such that
A1: not a,b,p are_collinear by Th14;
consider q being Element of FdSp such that
A2: parallelogram a,b,p,q by A1, Th34;
not p,q,b are_collinear by A2, Th28;
then consider c being Element of FdSp such that
A3: parallelogram p,q,b,c by Th34;
A4: p,q '||' b,c by A3;
( p <> q & a,b '||' p,q ) by A2, Th26;
then a,b '||' b,c by A4, PARSP_1:26;
then b,a '||' b,c by PARSP_1:23;
then b,a,c are_collinear ;
then A5: a,b,c are_collinear by Th10;
A6: not a,q '||' b,p by A2, Th36;
p,b '||' q,c by A3;
then A7: a <> c by A6, PARSP_1:23;
b <> c by A3, Th26;
hence ex c being Element of FdSp st
( a,b,c are_collinear & c <> a & c <> b ) by A7, A5; :: thesis: verum