theorem Th5: :: FINTOPO6:6

for FT being non empty RelStr
for A, B being Subset of FT st FT is symmetric & A ^b misses B holds
A misses B ^b