let I be set ; :: thesis: for A, M being ManySortedSet of I
for SF being SubsetFamily of M st A in SF holds
A in' |:SF:|
let A, M 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 object ; :: according to PBOOLE:def 1 :: 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, Th14;
hence A . i in |:SF:| . i by A1; :: thesis: verum