let I be set ; :: thesis: for M being ManySortedSet of I
for SFe being non-empty MSSubsetFamily of M holds meet SFe c= union SFe
let M be ManySortedSet of I; :: thesis: for SFe being non-empty MSSubsetFamily of M holds meet SFe c= union SFe
let SFe be non-empty MSSubsetFamily of M; :: thesis: meet SFe c= union SFe
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or (meet SFe) . i c= (union SFe) . i )
assume A1: i in I ; :: thesis: (meet SFe) . i c= (union SFe) . i
then consider Q being Subset-Family of (M . i) such that
A2: Q = SFe . i and
A3: (meet SFe) . i = Intersect Q by Def1;
( meet Q c= union Q & Intersect Q = meet Q ) by A1, A2, SETFAM_1:2, SETFAM_1:def 9;
hence (meet SFe) . i c= (union SFe) . i by A1, A2, A3, MBOOLEAN:def 2; :: thesis: verum