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:18, XBOOLE_1:28;
thus A ^deltao = (A ` ) /\ ((A ^b ) /\ ((A ` ) ^b )) by FIN_TOPO:24
.= (A ^b ) /\ ((A ` ) /\ ((A ` ) ^b )) by XBOOLE_1:16
.= (A ^b ) \ A by A1, SUBSET_1:32 ; :: thesis: verum