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 object holds
( x in ((A `) ^Foi) ` iff x in A ^Fob )

proof

let x be object ; :: 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 object such that
A3: z in W and
A4: not z in A ` ;
z in A by A3, A4, XBOOLE_0:def 5;
hence W meets A by A3, XBOOLE_0:3; :: thesis: verum

end;

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

end;

assume A5: 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 A5, Th20;
then ex z being object st
( z in W & z in A ) by XBOOLE_0:3;
hence not W c= A ` by XBOOLE_0:def 5; :: thesis: verum

end;

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

end;

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