let FMT be non empty FMT_Space_Str ; :: thesis: for A being Subset of FMT holds ((A ` ) ^Fob ) ` = A ^Foi
let A be Subset of FMT; :: thesis: ((A ` ) ^Fob ) ` = A ^Foi
for x being set holds
( x in ((A ` ) ^Fob ) ` iff x in A ^Foi )

proof

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

proof

assume A1: x in ((A ` ) ^Fob ) ` ; :: thesis: x in A ^Foi
then reconsider y = x as Element of FMT ;
not y in (A ` ) ^Fob by A1, XBOOLE_0:def 5;
then consider V being Subset of FMT such that
A2: ( V in U_FMT y & V misses A ` ) ;
V /\ (A ` ) = {} by A2, XBOOLE_0:def 7;
then ( V in U_FMT y & V \ A = {} ) by A2, SUBSET_1:32;
then ( V in U_FMT y & V c= A ) by XBOOLE_1:37;
hence x in A ^Foi ; :: thesis: verum

end;

assume A3: x in A ^Foi ; :: thesis: x in ((A ` ) ^Fob ) `
then reconsider y = x as Element of FMT ;
consider V being Subset of FMT such that
A4: ( V in U_FMT y & V c= A ) by A3, Th22;
( V in U_FMT y & V \ A = {} ) by A4, XBOOLE_1:37;
then ( V in U_FMT y & V /\ (A ` ) = {} ) by SUBSET_1:32;
then ( V in U_FMT y & V misses A ` ) by XBOOLE_0:def 7;
then not y in (A ` ) ^Fob by Th21;
hence x in ((A ` ) ^Fob ) ` by XBOOLE_0:def 5; :: thesis: verum

end;

hence ((A ` ) ^Fob ) ` = A ^Foi by TARSKI:2; :: thesis: verum