let G be IncProjStr ; :: thesis: for a, b, c being POINT of G holds
( a,b,c are_collinear iff ex P being LINE of G st
( a on P & b on P & c on P ) )
let a, b, c be POINT of G; :: thesis: ( a,b,c are_collinear iff ex P being LINE of G st
( a on P & b on P & c on P ) )
( ex P being LINE of G st {a,b,c} on P iff ex P being LINE of G st
( a on P & b on P & c on P ) )
proof
hereby :: thesis: ( ex P being LINE of G st
( a on P & b on P & c on P ) implies ex P being LINE of G st {a,b,c} on P )
given P being LINE of G such that A1: {a,b,c} on P ; :: thesis: ex P being LINE of G st
( a on P & b on P & c on P )
take P = P; :: thesis: ( a on P & b on P & c on P )
thus ( a on P & b on P & c on P ) by A1, INCSP_1:2; :: thesis: verum
end;
thus ( ex P being LINE of G st
( a on P & b on P & c on P ) implies ex P being LINE of G st {a,b,c} on P ) by INCSP_1:2; :: thesis: verum
end;
hence ( a,b,c are_collinear iff ex P being LINE of G st
( a on P & b on P & c on P ) ) ; :: thesis: verum