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 object holds

( x in (A `) ^delta iff x in A ^delta )

let A be Subset of FT; :: thesis: (A `) ^delta = A ^delta

for x being object holds

( x in (A `) ^delta iff x in A ^delta )

proof

hence
(A `) ^delta = A ^delta
by TARSKI:2; :: thesis: verum
let x be object ; :: 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 )

then reconsider y = x as Element of FT ;

( U_FT y meets (A `) ` & U_FT y meets A ` ) by A2, Th5;

hence x in (A `) ^delta ; :: thesis: verum

end;thus ( x in (A `) ^delta implies x in A ^delta ) :: thesis: ( x in A ^delta implies x in (A `) ^delta )

proof

assume A2:
x in A ^delta
; :: thesis: x in (A `) ^delta
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, Th5;

hence x in A ^delta ; :: thesis: verum

end;then reconsider y = x as Element of FT ;

( U_FT y meets A ` & U_FT y meets (A `) ` ) by A1, Th5;

hence x in A ^delta ; :: thesis: verum

then reconsider y = x as Element of FT ;

( U_FT y meets (A `) ` & U_FT y meets A ` ) by A2, Th5;

hence x in (A `) ^delta ; :: thesis: verum