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

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