let FT be non empty RelStr ; :: thesis: for A being Subset of FT holds (A ` ) ^delta = A ^delta
let A be Subset of FT; :: thesis: (A ` ) ^delta = A ^delta
for x being set holds
( x in (A ` ) ^delta iff x in A ^delta )

proof

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

proof

assume A1: x in (A ` ) ^delta ; :: thesis: x in A ^delta
then reconsider y = x as Element of FT ;
( U_FT y meets A ` & U_FT y meets (A ` ) ` ) by A1, Th10;
hence x in A ^delta ; :: thesis: verum

end;

assume A2: x in A ^delta ; :: thesis: x in (A ` ) ^delta
then reconsider y = x as Element of FT ;
( U_FT y meets (A ` ) ` & U_FT y meets A ` ) by A2, Th10;
hence x in (A ` ) ^delta ; :: thesis: verum

end;

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