let S be IncStruct ; :: thesis: for A, B, C, D being POINT of S

for P being PLANE of S holds

( {A,B,C,D} on P iff ( A on P & B on P & C on P & D on P ) )

let A, B, C, D be POINT of S; :: thesis: for P being PLANE of S holds

( {A,B,C,D} on P iff ( A on P & B on P & C on P & D on P ) )

let P be PLANE of S; :: thesis: ( {A,B,C,D} on P iff ( A on P & B on P & C on P & D on P ) )

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

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

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

hence E on P by A3, ENUMSET1:def 2; :: thesis: verum

for P being PLANE of S holds

( {A,B,C,D} on P iff ( A on P & B on P & C on P & D on P ) )

let A, B, C, D be POINT of S; :: thesis: for P being PLANE of S holds

( {A,B,C,D} on P iff ( A on P & B on P & C on P & D on P ) )

let P be PLANE of S; :: thesis: ( {A,B,C,D} on P iff ( A on P & B on P & C on P & D on P ) )

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

proof

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

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

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

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

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

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

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

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

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

hence E on P by A3, ENUMSET1:def 2; :: thesis: verum