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 )
proof
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) ` )
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 ;
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;
assume A4: 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
A5: V in U_FMT y and
A6: V c= A by ;
V \ A = {} by ;
then V /\ (A `) = {} by SUBSET_1:13;
then V misses A ` ;
then not y in (A `) ^Fob by ;
hence x in ((A `) ^Fob) ` by XBOOLE_0:def 5; :: thesis: verum
end;
hence ((A `) ^Fob) ` = A ^Foi by TARSKI:2; :: thesis: verum