let M be set ; :: thesis: for B1, B2 being Subset-Family of M holds (Intersect B1) /\ (Intersect B2) c= Intersect (B1 /\ B2)
let B1, B2 be Subset-Family of M; :: thesis: (Intersect B1) /\ (Intersect B2) c= Intersect (B1 /\ B2)
Intersect (B1 \/ B2) c= Intersect (B1 /\ B2) by SETFAM_1:44, XBOOLE_1:29;
hence (Intersect B1) /\ (Intersect B2) c= Intersect (B1 /\ B2) by MSSUBFAM:8; :: thesis: verum