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 )

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

hence
((A `) ^Foi) ` = A ^Fob
by TARSKI:2; :: thesis: verum
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) ` )

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 `

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

end;thus ( x in ((A `) ^Foi) ` implies x in A ^Fob ) :: thesis: ( x in A ^Fob implies x in ((A `) ^Foi) ` )

proof

assume A5:
x in A ^Fob
; :: thesis: x in ((A `) ^Foi) `
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

end;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

hence
x in A ^Fob
; :: thesis: verum
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;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

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

then
not y in (A `) ^Foi
by Th21;
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;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

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