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