let S be IncStruct ; :: thesis: for A, B, C being POINT of S
for P being PLANE of S holds
( {A,B,C} on P iff ( A on P & B on P & C on P ) )
let A, B, C be POINT of S; :: thesis: for P being PLANE of S holds
( {A,B,C} on P iff ( A on P & B on P & C on P ) )
let P be PLANE of S; :: thesis: ( {A,B,C} on P iff ( A on P & B on P & C on P ) )
thus ( {A,B,C} on P implies ( A on P & B on P & C on P ) ) :: thesis: ( A on P & B on P & C on P implies {A,B,C} on P )

proof

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 P ; :: thesis: ( A on P & B on P & C on P )
hence ( A on P & B on P & C on P ) by A2, A1; :: thesis: verum

end;

assume A3: ( A on P & B on P & C on P ) ; :: thesis: {A,B,C} on P
let D be POINT of S; :: according to INCSP_1:def 5 :: thesis: ( D in {A,B,C} implies D on P )
assume D in {A,B,C} ; :: thesis: D on P
hence D on P by A3, ENUMSET1:def 1; :: thesis: verum