theorem Th8: :: WAYBEL30:8

for T being non empty reflexive RelStr holds sigma T c= { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) }