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

proof

let x be set ; :: thesis: ( x in ((A ` ) ^b ) ` iff x in A ^i )
thus ( x in ((A ` ) ^b ) ` implies x in A ^i ) :: thesis: ( x in A ^i implies x in ((A ` ) ^b ) ` )

proof

assume A1: x in ((A ` ) ^b ) ` ; :: thesis: x in A ^i
then reconsider y = x as Element of FT ;
not y in (A ` ) ^b by A1, XBOOLE_0:def 5;
then U_FT y misses A ` ;
then (U_FT y) /\ (A ` ) = {} by XBOOLE_0:def 7;
then (U_FT y) \ A = {} by SUBSET_1:32;
then U_FT y c= A by XBOOLE_1:37;
hence x in A ^i ; :: thesis: verum

end;

assume A2: x in A ^i ; :: thesis: x in ((A ` ) ^b ) `
then reconsider y = x as Element of FT ;
U_FT y c= A by A2, Th12;
then (U_FT y) \ A = {} by XBOOLE_1:37;
then (U_FT y) /\ (A ` ) = {} by SUBSET_1:32;
then U_FT y misses A ` by XBOOLE_0:def 7;
then not y in (A ` ) ^b by Th13;
hence x in ((A ` ) ^b ) ` by SUBSET_1:50; :: thesis: verum

end;

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