let I be set ; :: thesis: for M being ManySortedSet of I
for SF being SubsetFamily of M
for Z being ManySortedSubset of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c=' Z1 ) holds
Z c=' meet |:SF:|
let M be ManySortedSet of I; :: thesis: for SF being SubsetFamily of M
for Z being ManySortedSubset of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c=' Z1 ) holds
Z c=' meet |:SF:|
let SF be SubsetFamily of M; :: thesis: for Z being ManySortedSubset of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c=' Z1 ) holds
Z c=' meet |:SF:|
let Z be ManySortedSubset of M; :: thesis: ( ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c=' Z1 ) implies Z c=' meet |:SF:| )
assume A1: for Z1 being ManySortedSet of I st Z1 in SF holds
Z c=' Z1 ; :: thesis: Z c=' meet |:SF:|
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or Z . i c= (meet |:SF:|) . i )
assume A2: i in I ; :: thesis: Z . i c= (meet |:SF:|) . i
consider Q being Subset-Family of (M . i) such that
A3: Q = |:SF:| . i and
A4: (meet |:SF:|) . i = Intersect Q by A2, MSSUBFAM:def 1;
A5: now :: thesis: for q being set st q in Q holds
Z . i c= q
let q be set ; :: thesis: ( q in Q implies Z . i c= b1 )
assume A6: q in Q ; :: thesis: Z . i c= b1
per cases ( not SF is empty or SF is empty ) ;
suppose not SF is empty ; :: thesis: Z . i c= b1
then |:SF:| . i = { (x . i) where x is Element of Bool M : x in SF } by A2, Th14;
then consider a being Element of Bool M such that
A7: q = a . i and
A8: a in SF by A3, A6;
Z c=' a by A1, A8;
hence Z . i c= q by A2, A7; :: thesis: verum
end;
end;
end;
Z c= M by PBOOLE:def 18;
then Z . i is Subset of (M . i) by A2;
hence Z . i c= (meet |:SF:|) . i by A4, A5, MSSUBFAM:4; :: thesis: verum