let i be object ; :: thesis: ( i in I implies ((meet SF) (/\) B) . i = (EmptyMS I) . i )
assume A3: i in I ; :: thesis: ((meet SF) (/\) B) . i = (EmptyMS I) . i
then consider Q being Subset-Family of (M . i) such that
A4: Q = SF . i and
A5: (meet SF) . i = Intersect Q by Def1;
A6: A . i in SF . i by A1, A3;
(A . i) /\ (B . i) = (EmptyMS I) . i by A2, A3, PBOOLE:def 5;
then (A . i) /\ (B . i) = {} ;
then A . i misses B . i ;
then meet Q misses B . i by A4, A6, SETFAM_1:8;
then (meet Q) /\ (B . i) = {} ;
then A7: (meet Q) /\ (B . i) = (EmptyMS I) . i ;
Intersect Q = meet Q by A4, A6, SETFAM_1:def 9;
hence ((meet SF) (/\) B) . i = (EmptyMS I) . i by A3, A5, A7, PBOOLE:def 5; :: thesis: verum