theorem Th55: :: EQREL_1:55

for X being set
for D being Subset-Family of X st union D = X holds
for A being Subset of D
for B being Subset of X st B = union A holds
B ` c= union (A `)