let I be set ; :: thesis: for M being ManySortedSet of I
for SF being MSSubsetFamily of M holds union SF c= M
let M be ManySortedSet of I; :: thesis: for SF being MSSubsetFamily of M holds union SF c= M
let SF be MSSubsetFamily of M; :: thesis: union SF c= M
A1: for x being set
for F being Subset-Family of x holds union F is Subset of x ;
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or (union SF) . i c= M . i )
assume A2: i in I ; :: thesis: (union SF) . i c= M . i
SF . i is Subset-Family of (M . i) by A2, Th32;
then union (SF . i) is Subset of (M . i) by A1;
then union (SF . i) c= M . i ;
hence (union SF) . i c= M . i by A2, MBOOLEAN:def 2; :: thesis: verum