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

for A, B, C being POINT of S holds

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

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

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

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

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

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

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

hence D on L by A3, ENUMSET1:def 1; :: thesis: verum

for A, B, C being POINT of S holds

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

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

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

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

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

proof

assume A3:
( A on L & B on L & C on L )
; :: thesis: {A,B,C} on L
A1:
C in {A,B,C}
by ENUMSET1:def 1;

A2: ( A in {A,B,C} & B in {A,B,C} ) by ENUMSET1:def 1;

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

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

end;A2: ( A in {A,B,C} & B in {A,B,C} ) by ENUMSET1:def 1;

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

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

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

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

hence D on L by A3, ENUMSET1:def 1; :: thesis: verum