let S be IncStruct ; :: thesis: for P being PLANE of S

for F, G being Subset of the Points of S holds

( F \/ G on P iff ( F on P & G on P ) )

let P be PLANE of S; :: thesis: for F, G being Subset of the Points of S holds

( F \/ G on P iff ( F on P & G on P ) )

let F, G be Subset of the Points of S; :: thesis: ( F \/ G on P iff ( F on P & G on P ) )

thus ( F \/ G on P implies ( F on P & G on P ) ) by Th7, XBOOLE_1:7; :: thesis: ( F on P & G on P implies F \/ G on P )

assume A1: ( F on P & G on P ) ; :: thesis: F \/ G on P

let C be POINT of S; :: according to INCSP_1:def 5 :: thesis: ( C in F \/ G implies C on P )

assume C in F \/ G ; :: thesis: C on P

then ( C in F or C in G ) by XBOOLE_0:def 3;

hence C on P by A1; :: thesis: verum

for F, G being Subset of the Points of S holds

( F \/ G on P iff ( F on P & G on P ) )

let P be PLANE of S; :: thesis: for F, G being Subset of the Points of S holds

( F \/ G on P iff ( F on P & G on P ) )

let F, G be Subset of the Points of S; :: thesis: ( F \/ G on P iff ( F on P & G on P ) )

thus ( F \/ G on P implies ( F on P & G on P ) ) by Th7, XBOOLE_1:7; :: thesis: ( F on P & G on P implies F \/ G on P )

assume A1: ( F on P & G on P ) ; :: thesis: F \/ G on P

let C be POINT of S; :: according to INCSP_1:def 5 :: thesis: ( C in F \/ G implies C on P )

assume C in F \/ G ; :: thesis: C on P

then ( C in F or C in G ) by XBOOLE_0:def 3;

hence C on P by A1; :: thesis: verum