theorem :: FINTOPO6:22

for FT being non empty filled RelStr
for A being Subset of FT holds A ^deltao = (A ^b) \ A