theorem :: FIN_TOPO:18

for FT being non empty RelStr
for A being Subset of FT holds A ^delta = (A ^b) /\ ((A `) ^b)