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

proof

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

proof

assume A1: x in ((A ` ) ^i ) ` ; :: thesis: x in A ^b
then reconsider y = x as Element of FT ;
not y in (A ` ) ^i by A1, XBOOLE_0:def 5;
then not U_FT y c= A ` ;
then consider z being set such that
A2: ( z in U_FT y & not z in A ` ) by TARSKI:def 3;
( z in U_FT y & z in A ) by A2, SUBSET_1:50;
then U_FT y meets A by XBOOLE_0:3;
hence x in A ^b ; :: thesis: verum

end;

assume A3: x in A ^b ; :: thesis: x in ((A ` ) ^i ) `
then reconsider y = x as Element of FT ;
U_FT y meets A by A3, Th13;
then consider z being set such that
A4: ( z in U_FT y & z in A ) by XBOOLE_0:3;
not U_FT y c= A ` by A4, XBOOLE_0:def 5;
then not y in (A ` ) ^i by Th12;
hence x in ((A ` ) ^i ) ` by SUBSET_1:50; :: thesis: verum

end;

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