theorem Th2: :: TOPS_2:2

for T being 1-sorted
for F being Subset-Family of T
for X being set st X c= F holds
X is Subset-Family of T