let n be Element of NAT ; :: thesis: for B, X, Y being Subset of (TOP-REAL n) holds B (+) (X /\ Y) c= (B (+) X) /\ (B (+) Y)
let B, X, Y be Subset of (TOP-REAL n); :: thesis: B (+) (X /\ Y) c= (B (+) X) /\ (B (+) Y)
B (+) (X /\ Y) = (X /\ Y) (+) B by Th12;
then B (+) (X /\ Y) c= (X (+) B) /\ (Y (+) B) by Th34;
then B (+) (X /\ Y) c= (B (+) X) /\ (Y (+) B) by Th12;
hence B (+) (X /\ Y) c= (B (+) X) /\ (B (+) Y) by Th12; :: thesis: verum