let I be set ; :: thesis: for M, A being ManySortedSet of I
for SF being SubsetFamily of M st A in SF holds
A in' |:SF:|
let M, A be ManySortedSet of I; :: thesis: for SF being SubsetFamily of M st A in SF holds
A in' |:SF:|
let SF be SubsetFamily of M; :: thesis: ( A in SF implies A in' |:SF:| )
assume A1: A in SF ; :: thesis: A in' |:SF:|
let i be set ; :: according to PBOOLE:def 4 :: thesis: ( not i in I or A . i in |:SF:| . i )
assume i in I ; :: thesis: A . i in |:SF:| . i
then |:SF:| . i = { (x . i) where x is Element of Bool M : x in SF } by A1, Th15;
hence A . i in |:SF:| . i by A1; :: thesis: verum