:: deftheorem defines ^deltao FIN_TOPO:def 7 :
for FT being non empty RelStr
for A being Subset of FT holds A ^deltao = (A `) /\ (A ^delta);