INTERSECTION (F,G) c= bool T

proof

hence
INTERSECTION (F,G) is Subset-Family of T
; :: thesis: verum
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;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