let I be set ; for A, B, M being ManySortedSet of I
for SF being MSSubsetFamily of M st A in SF & A c= B holds
meet SF c= B
let A, B, M be ManySortedSet of I; for SF being MSSubsetFamily of M st A in SF & A c= B holds
meet SF c= B
let SF be MSSubsetFamily of M; ( A in SF & A c= B implies meet SF c= B )
assume that
A1:
A in SF
and
A2:
A c= B
; meet SF c= B
let i be object ; PBOOLE:def 2 ( not i in I or (meet SF) . i c= B . i )
assume A3:
i in I
; (meet SF) . i c= B . i
then A4:
A . i c= B . i
by A2;
consider Q being Subset-Family of (M . i) such that
A5:
Q = SF . i
and
A6:
(meet SF) . i = Intersect Q
by A3, Def1;
A7:
A . i in SF . i
by A1, A3;
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; verum