let X be set ; :: thesis: for F, G being Subset-Family of X holds COMPLEMENT (F \/ G) = (COMPLEMENT F) \/ (COMPLEMENT G)
let F, G be Subset-Family of X; :: thesis: COMPLEMENT (F \/ G) = (COMPLEMENT F) \/ (COMPLEMENT G)
for P being Subset of X holds
( P in (COMPLEMENT F) \/ (COMPLEMENT G) iff P ` in F \/ G )
proof
let P be Subset of X; :: thesis: ( P in (COMPLEMENT F) \/ (COMPLEMENT G) iff P ` in F \/ G )
( ( ( not P in COMPLEMENT F & not P in COMPLEMENT G ) or P ` in F or P ` in G ) & ( ( not P ` in F & not P ` in G ) or P in COMPLEMENT F or P in COMPLEMENT G ) ) by Def7;
hence ( P in (COMPLEMENT F) \/ (COMPLEMENT G) iff P ` in F \/ G ) by XBOOLE_0:def 3; :: thesis: verum
end;
hence COMPLEMENT (F \/ G) = (COMPLEMENT F) \/ (COMPLEMENT G) by Def7; :: thesis: verum