let FT be non empty RelStr ; :: thesis: for A being Subset of FT holds A ^delta = (A ^b) \ (A ^i)
let A be Subset of FT; :: thesis: A ^delta = (A ^b) \ (A ^i)
for x being object holds
( x in A ^delta iff x in (A ^b) \ (A ^i) )

proof

let x be object ; :: thesis: ( x in A ^delta iff x in (A ^b) \ (A ^i) )
thus ( x in A ^delta implies x in (A ^b) \ (A ^i) ) :: thesis: ( x in (A ^b) \ (A ^i) implies x in A ^delta )

proof

assume x in A ^delta ; :: thesis: x in (A ^b) \ (A ^i)
then x in (A ^b) /\ ((A ^i) `) by Th2;
hence x in (A ^b) \ (A ^i) by SUBSET_1:13; :: thesis: verum

end;

assume x in (A ^b) \ (A ^i) ; :: thesis: x in A ^delta
then x in (A ^b) /\ ((A ^i) `) by SUBSET_1:13;
hence x in A ^delta by Th2; :: thesis: verum

end;

hence A ^delta = (A ^b) \ (A ^i) by TARSKI:2; :: thesis: verum