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

proof

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

proof

assume A1: x in ((A ` ) ^Foi ) ` ; :: thesis: x in A ^Fob
then reconsider y = x as Element of FMT ;
A2: not y in (A ` ) ^Foi by A1, XBOOLE_0:def 5;
for W being Subset of FMT st W in U_FMT y holds
W meets A

proof

let W be Subset of FMT; :: thesis: ( W in U_FMT y implies W meets A )
assume W in U_FMT y ; :: thesis: W meets A
then not W c= A ` by A2;
then consider z being set such that
A3: ( z in W & not z in A ` ) by TARSKI:def 3;
( z in W & z in A ) by A3, XBOOLE_0:def 5;
hence W meets A by XBOOLE_0:3; :: thesis: verum

end;

hence x in A ^Fob ; :: thesis: verum

end;

assume A4: x in A ^Fob ; :: thesis: x in ((A ` ) ^Foi ) `
then reconsider y = x as Element of FMT ;
for W being Subset of FMT st W in U_FMT y holds
not W c= A `

proof

let W be Subset of FMT; :: thesis: ( W in U_FMT y implies not W c= A ` )
assume W in U_FMT y ; :: thesis: not W c= A `
then W meets A by A4, Th21;
then consider z being set such that
A5: ( z in W & z in A ) by XBOOLE_0:3;
thus not W c= A ` by A5, XBOOLE_0:def 5; :: thesis: verum

end;

then not y in (A ` ) ^Foi by Th22;
hence x in ((A ` ) ^Foi ) ` by XBOOLE_0:def 5; :: thesis: verum

end;

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