theorem Th28: :: FINTOPO6:29

for FT being non empty RelStr
for A, B, A1, B1 being Subset of FT st A,B are_separated & A1 c= A & B1 c= B holds
A1,B1 are_separated