INTERSECTION (F,G) c= bool T
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in INTERSECTION (F,G) or x in bool T )
assume x in INTERSECTION (F,G) ; :: thesis: x in bool T
then consider X, Y being set such that
A1: X in F and
Y in G and
A2: x = X /\ Y by SETFAM_1:def 5;
X /\ Y c= X by XBOOLE_1:17;
then x is Subset of T by A1, A2, XBOOLE_1:1;
hence x in bool T ; :: thesis: verum
end;
hence INTERSECTION (F,G) is Subset-Family of T ; :: thesis: verum