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 ;
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 ;
hence W meets A by ; :: 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 ;
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