UNION (F,G) c= bool T

proof

hence
UNION (F,G) is Subset-Family of T
; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UNION (F,G) or x in bool T )

assume x in UNION (F,G) ; :: thesis: x in bool T

then consider X, Y being set such that

A3: ( X in F & Y in G ) and

A4: x = X \/ Y by SETFAM_1:def 4;

X \/ Y c= T by A3, XBOOLE_1:8;

hence x in bool T by A4; :: thesis: verum

end;assume x in UNION (F,G) ; :: thesis: x in bool T

then consider X, Y being set such that

A3: ( X in F & Y in G ) and

A4: x = X \/ Y by SETFAM_1:def 4;

X \/ Y c= T by A3, XBOOLE_1:8;

hence x in bool T by A4; :: thesis: verum