theorem Th2: :: FINTOPO2:2

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