let I be set ; :: thesis: for M, A being ManySortedSet of
for SF being MSSubsetFamily of M st A in meet SF holds
for B being ManySortedSet of st B in SF holds
A in B
let M, A be ManySortedSet of ; :: thesis: for SF being MSSubsetFamily of M st A in meet SF holds
for B being ManySortedSet of st B in SF holds
A in B
let SF be MSSubsetFamily of M; :: thesis: ( A in meet SF implies for B being ManySortedSet of st B in SF holds
A in B )
assume A1: A in meet SF ; :: thesis: for B being ManySortedSet of st B in SF holds
A in B
let B be ManySortedSet of ; :: thesis: ( B in SF implies A in B )
assume A2: B in SF ; :: thesis: A in B
let i be set ; :: according to PBOOLE:def 4 :: thesis: ( not i in I or A . i in B . i )
assume A3: i in I ; :: thesis: A . i in B . 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 (meet SF) . i by A1, A3, PBOOLE:def 4;
B . i in SF . i by A2, A3, PBOOLE:def 4;
hence A . i in B . i by A4, A5, A6, SETFAM_1:58; :: thesis: verum