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 ) )

( a on P & b on P & c on P ) ) ; :: thesis: verum

( 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

( 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 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 )

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 )

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;( 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

( 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

( a on P & b on P & c on P ) ) ; :: thesis: verum