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

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