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 object holds

( x in ((A `) ^Fob) ` iff x in A ^Foi )

let A be Subset of FMT; :: thesis: ((A `) ^Fob) ` = A ^Foi

for x being object holds

( x in ((A `) ^Fob) ` iff x in A ^Foi )

proof

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

then reconsider y = x as Element of FMT ;

consider V being Subset of FMT such that

A5: V in U_FMT y and

A6: V c= A by A4, Th21;

V \ A = {} by A6, XBOOLE_1:37;

then V /\ (A `) = {} by SUBSET_1:13;

then V misses A ` ;

then not y in (A `) ^Fob by A5, Th20;

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

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

proof

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

A3: V misses A ` ;

V /\ (A `) = {} by A3;

then V \ A = {} by SUBSET_1:13;

then V c= A by XBOOLE_1:37;

hence x in A ^Foi by A2; :: thesis: verum

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

A3: V misses A ` ;

V /\ (A `) = {} by A3;

then V \ A = {} by SUBSET_1:13;

then V c= A by XBOOLE_1:37;

hence x in A ^Foi by A2; :: thesis: verum

then reconsider y = x as Element of FMT ;

consider V being Subset of FMT such that

A5: V in U_FMT y and

A6: V c= A by A4, Th21;

V \ A = {} by A6, XBOOLE_1:37;

then V /\ (A `) = {} by SUBSET_1:13;

then V misses A ` ;

then not y in (A `) ^Fob by A5, Th20;

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