theorem Th1: :: FINTOPO3:1

for T being non empty RelStr
for A being Subset of T st T is filled holds
A c= A ^f