let I be set ; :: thesis: for M being ManySortedSet of
for SF, SG being MSSubsetFamily of M st SF c= SG holds
meet SG c= meet SF
let M be ManySortedSet of ; :: thesis: for SF, SG being MSSubsetFamily of M st SF c= SG holds
meet SG c= meet SF
let SF, SG be MSSubsetFamily of M; :: thesis: ( SF c= SG implies meet SG c= meet SF )
assume A1: SF c= SG ; :: thesis: meet SG c= meet SF
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or (meet SG) . i c= (meet SF) . i )
assume A2: i in I ; :: thesis: (meet SG) . i c= (meet SF) . i
then consider Qf being Subset-Family of (M . i) such that
A3: Qf = SF . i and
A4: (meet SF) . i = Intersect Qf by Def2;
consider Qg being Subset-Family of (M . i) such that
A5: Qg = SG . i and
A6: (meet SG) . i = Intersect Qg by A2, Def2;
Qf c= Qg by A1, A2, A3, A5, PBOOLE:def 5;
hence (meet SG) . i c= (meet SF) . i by A4, A6, SETFAM_1:59; :: thesis: verum