let X, Y be set ; :: thesis: for F being Subset-Family of X
for G being Subset-Family of Y holds F \/ G is Subset-Family of (X \/ Y)
let F be Subset-Family of X; :: thesis: for G being Subset-Family of Y holds F \/ G is Subset-Family of (X \/ Y)
let G be Subset-Family of Y; :: thesis: F \/ G is Subset-Family of (X \/ Y)
A1: F \/ G c= (bool X) \/ (bool Y) by XBOOLE_1:13;
(bool X) \/ (bool Y) c= bool (X \/ Y) by ZFMISC_1:69;
hence F \/ G is Subset-Family of (X \/ Y) by A1, XBOOLE_1:1; :: thesis: verum