let FT be non empty filled RelStr ; :: thesis: for A being Subset of FT holds A ^deltao = (A ^b) \ A
let A be Subset of FT; :: thesis: A ^deltao = (A ^b) \ A
A1: (A `) /\ ((A `) ^b) = A ` by FIN_TOPO:13, XBOOLE_1:28;
thus A ^deltao = (A `) /\ ((A ^b) /\ ((A `) ^b)) by FIN_TOPO:18
.= (A ^b) /\ ((A `) /\ ((A `) ^b)) by XBOOLE_1:16
.= (A ^b) \ A by A1, SUBSET_1:13 ; :: thesis: verum