let I be set ; :: thesis: for A, M being ManySortedSet of I
for SF being MSSubsetFamily of M st A in meet SF holds
for B being ManySortedSet of I st B in SF holds
A in B
let A, M be ManySortedSet of I; :: thesis: for SF being MSSubsetFamily of M st A in meet SF holds
for B being ManySortedSet of I 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 I st B in SF holds
A in B )
assume A1: A in meet SF ; :: thesis: for B being ManySortedSet of I st B in SF holds
A in B
let B be ManySortedSet of I; :: thesis: ( B in SF implies A in B )
assume A2: B in SF ; :: thesis: A in B
let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or A . i in B . i )
assume A3: i in I ; :: thesis: A . i in B . i
then A4: A . i in (meet SF) . i by A1;
A5: B . i in SF . i by A2, A3;
ex Q being Subset-Family of (M . i) st
( Q = SF . i & (meet SF) . i = Intersect Q ) by A3, Def1;
hence A . i in B . i by A4, A5, SETFAM_1:43; :: thesis: verum