let I be set ; :: thesis: for M, A, B being ManySortedSet of I
for SF being MSSubsetFamily of M st A in SF & A c= B holds
meet SF c= B
let M, A, B be ManySortedSet of I; :: thesis: for SF being MSSubsetFamily of M st A in SF & A c= B holds
meet SF c= B
let SF be MSSubsetFamily of M; :: thesis: ( A in SF & A c= B implies meet SF c= B )
assume that
A1: A in SF and
A2: A c= B ; :: thesis: meet SF c= B
let i be set ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or (meet SF) . i c= B . i )
assume A3: i in I ; :: thesis: (meet SF) . i c= B . i
then A4: A . i c= B . i by A2, PBOOLE:def 2;
consider Q being Subset-Family of (M . i) such that
A5: Q = SF . i and
A6: (meet SF) . i = Intersect Q by A3, Def2;
A7: A . i in SF . i by A1, A3, PBOOLE:def 1;
then Intersect Q = meet Q by A5, SETFAM_1:def 9;
hence (meet SF) . i c= B . i by A5, A6, A7, A4, SETFAM_1:7; :: thesis: verum