let S be IncProjStr ; 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; 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; ( {A,B} on L iff ( A on L & B on L ) )
thus
( {A,B} on L implies ( A on L & B on L ) )
( A on L & B on L implies {A,B} on L )
assume A2:
( A on L & B on L )
; {A,B} on L
let C be POINT of S; INCSP_1:def 4 ( C in {A,B} implies C on L )
assume
C in {A,B}
; C on L
hence
C on L
by A2, TARSKI:def 2; verum