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