let S be IncProjStr ; :: thesis: for L being LINE of S

for A, B being POINT of S holds

( {A,B} on L iff ( A on L & B on L ) )

let L be LINE of S; :: thesis: for A, B being POINT of S holds

( {A,B} on L iff ( A on L & B on L ) )

let A, B be POINT of S; :: thesis: ( {A,B} on L iff ( A on L & B on L ) )

thus ( {A,B} on L implies ( A on L & B on L ) ) :: thesis: ( A on L & B on L implies {A,B} on L )

let C be POINT of S; :: according to INCSP_1:def 4 :: thesis: ( C in {A,B} implies C on L )

assume C in {A,B} ; :: thesis: C on L

hence C on L by A2, TARSKI:def 2; :: thesis: verum

for A, B being POINT of S holds

( {A,B} on L iff ( A on L & B on L ) )

let L be LINE of S; :: thesis: for A, B being POINT of S holds

( {A,B} on L iff ( A on L & B on L ) )

let A, B be POINT of S; :: thesis: ( {A,B} on L iff ( A on L & B on L ) )

thus ( {A,B} on L implies ( A on L & B on L ) ) :: thesis: ( A on L & B on L implies {A,B} on L )

proof

assume A2:
( A on L & B on L )
; :: thesis: {A,B} on L
A1:
( A in {A,B} & B in {A,B} )
by TARSKI:def 2;

assume {A,B} on L ; :: thesis: ( A on L & B on L )

hence ( A on L & B on L ) by A1; :: thesis: verum

end;assume {A,B} on L ; :: thesis: ( A on L & B on L )

hence ( A on L & B on L ) by A1; :: thesis: verum

let C be POINT of S; :: according to INCSP_1:def 4 :: thesis: ( C in {A,B} implies C on L )

assume C in {A,B} ; :: thesis: C on L

hence C on L by A2, TARSKI:def 2; :: thesis: verum