let T be TopSpace; :: thesis: for F, G being Subset-Family of T holds Int (F /\ G) c= (Int F) /\ (Int G)
let F, G be Subset-Family of T; :: thesis: Int (F /\ G) c= (Int F) /\ (Int G)
for X being object st X in Int (F /\ G) holds
X in (Int F) /\ (Int G)
proof
let X be object ; :: thesis: ( X in Int (F /\ G) implies X in (Int F) /\ (Int G) )
assume A1: X in Int (F /\ G) ; :: thesis: X in (Int F) /\ (Int G)
then reconsider X0 = X as Subset of T ;
consider W being Subset of T such that
A2: X0 = Int W and
A3: W in F /\ G by A1, Def1;
W in G by A3, XBOOLE_0:def 4;
then A4: X0 in Int G by A2, Def1;
W in F by A3, XBOOLE_0:def 4;
then X0 in Int F by A2, Def1;
hence X in (Int F) /\ (Int G) by A4, XBOOLE_0:def 4; :: thesis: verum
end;
hence Int (F /\ G) c= (Int F) /\ (Int G) ; :: thesis: verum