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 set holds
( x in A ^d iff x in ((A ` ) ^f ) ` )

proof

let x be set ; :: thesis: ( x in A ^d iff x in ((A ` ) ^f ) ` )
thus ( x in A ^d implies x in ((A ` ) ^f ) ` ) :: thesis: ( x in ((A ` ) ^f ) ` implies x in A ^d )

proof

assume A1: x in A ^d ; :: thesis: x in ((A ` ) ^f ) `
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 14;
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 A1, Th2;
then not x in (A ` ) ^f by A2;
hence x in ((A ` ) ^f ) ` by A1, SUBSET_1:50; :: thesis: verum

end;

assume A3: x in ((A ` ) ^f ) ` ; :: thesis: x in A ^d
then A4: not x in (A ` ) ^f by XBOOLE_0:def 5;
(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 14;
then for y being Element of T st y in A ` holds
not x in U_FT y by A4;
hence x in A ^d by A3; :: thesis: verum

end;

hence A ^d = ((A ` ) ^f ) ` by TARSKI:2; :: thesis: verum