let S be IncStruct ; :: thesis: for L being LINE of S
for F, G being Subset of the Points of S holds
( F \/ G on L iff ( F on L & G on L ) )
let L be LINE of S; :: thesis: for F, G being Subset of the Points of S holds
( F \/ G on L iff ( F on L & G on L ) )
let F, G be Subset of the Points of S; :: thesis: ( F \/ G on L iff ( F on L & G on L ) )
thus ( F \/ G on L implies ( F on L & G on L ) ) by Th6, XBOOLE_1:7; :: thesis: ( F on L & G on L implies F \/ G on L )
assume A1: ( F on L & G on L ) ; :: thesis: F \/ G on L
let C be POINT of S; :: according to INCSP_1:def 4 :: thesis: ( C in F \/ G implies C on L )
assume C in F \/ G ; :: thesis: C on L
then ( C in F or C in G ) by XBOOLE_0:def 3;
hence C on L by A1; :: thesis: verum