let T be non empty RelStr ; :: thesis: for A being Subset of T holds A ^d = ((A `) ^f) `
let A be Subset of T; :: thesis: A ^d = ((A `) ^f) `
for x being object holds
( x in A ^d iff x in ((A `) ^f) ` )
proof
let x be object ; :: thesis: ( x in A ^d iff x in ((A `) ^f) ` )
A1: (A `) ^f = { x2 where x2 is Element of T : ex y being Element of T st
( y in A ` & x2 in U_FT y ) } by FIN_TOPO:def 12;
thus ( x in A ^d implies x in ((A `) ^f) ` ) :: thesis: ( x in ((A `) ^f) ` implies x in A ^d )
proof
A2: (A `) ^f = { x2 where x2 is Element of T : ex y being Element of T st
( y in A ` & x2 in U_FT y ) } by FIN_TOPO:def 12;
assume A3: x in A ^d ; :: thesis: x in ((A `) ^f) `
then for x2 being Element of T holds
( not x2 = x or for y being Element of T holds
( not y in A ` or not x2 in U_FT y ) ) by Th2;
then not x in (A `) ^f by A2;
hence x in ((A `) ^f) ` by A3, SUBSET_1:29; :: thesis: verum
end;
assume A4: x in ((A `) ^f) ` ; :: thesis: x in A ^d
then not x in (A `) ^f by XBOOLE_0:def 5;
then for y being Element of T st y in A ` holds
not x in U_FT y by A1;
hence x in A ^d by A4; :: thesis: verum
end;
hence A ^d = ((A `) ^f) ` by TARSKI:2; :: thesis: verum