let I be set ; :: thesis: for M, A, B being ManySortedSet of
for SF being MSSubsetFamily of M st A in SF & A /\ B = [0] I holds
(meet SF) /\ B = [0] I
let M, A, B be ManySortedSet of ; :: thesis: for SF being MSSubsetFamily of M st A in SF & A /\ B = [0] I holds
(meet SF) /\ B = [0] I
let SF be MSSubsetFamily of M; :: thesis: ( A in SF & A /\ B = [0] I implies (meet SF) /\ B = [0] I )
assume that
A1: A in SF and
A2: A /\ B = [0] I ; :: thesis: (meet SF) /\ B = [0] I

now

let i be set ; :: thesis: ( i in I implies ((meet SF) /\ B) . i = ([0] I) . i )
assume A3: i in I ; :: thesis: ((meet SF) /\ B) . i = ([0] 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 Def2;
A6: A . i in SF . i by A1, A3, PBOOLE:def 4;
then A7: Intersect Q = meet Q by A4, SETFAM_1:def 10;
(A . i) /\ (B . i) = ([0] I) . i by A2, A3, PBOOLE:def 8;
then (A . i) /\ (B . i) = {} by PBOOLE:5;
then A . i misses B . i by XBOOLE_0:def 7;
then meet Q misses B . i by A4, A6, SETFAM_1:9;
then (meet Q) /\ (B . i) = {} by XBOOLE_0:def 7;
then (meet Q) /\ (B . i) = ([0] I) . i by PBOOLE:5;
hence ((meet SF) /\ B) . i = ([0] I) . i by A3, A5, A7, PBOOLE:def 8; :: thesis: verum

end;

hence (meet SF) /\ B = [0] I by PBOOLE:3; :: thesis: verum