let FT be non empty RelStr ; :: thesis: for A being Subset of FT holds ((A `) ^b) ` = A ^i

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

for x being object holds

( x in ((A `) ^b) ` iff x in A ^i )

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

for x being object holds

( x in ((A `) ^b) ` iff x in A ^i )

proof

hence
((A `) ^b) ` = A ^i
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in ((A `) ^b) ` iff x in A ^i )

thus ( x in ((A `) ^b) ` implies x in A ^i ) :: thesis: ( x in A ^i implies x in ((A `) ^b) ` )

then reconsider y = x as Element of FT ;

U_FT y c= A by A2, Th7;

then (U_FT y) \ A = {} by XBOOLE_1:37;

then (U_FT y) /\ (A `) = {} by SUBSET_1:13;

then U_FT y misses A ` ;

then not y in (A `) ^b by Th8;

hence x in ((A `) ^b) ` by SUBSET_1:29; :: thesis: verum

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

proof

assume A2:
x in A ^i
; :: thesis: x in ((A `) ^b) `
assume A1:
x in ((A `) ^b) `
; :: thesis: x in A ^i

then reconsider y = x as Element of FT ;

not y in (A `) ^b by A1, XBOOLE_0:def 5;

then U_FT y misses A ` ;

then (U_FT y) /\ (A `) = {} ;

then (U_FT y) \ A = {} by SUBSET_1:13;

then U_FT y c= A by XBOOLE_1:37;

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

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

not y in (A `) ^b by A1, XBOOLE_0:def 5;

then U_FT y misses A ` ;

then (U_FT y) /\ (A `) = {} ;

then (U_FT y) \ A = {} by SUBSET_1:13;

then U_FT y c= A by XBOOLE_1:37;

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

then reconsider y = x as Element of FT ;

U_FT y c= A by A2, Th7;

then (U_FT y) \ A = {} by XBOOLE_1:37;

then (U_FT y) /\ (A `) = {} by SUBSET_1:13;

then U_FT y misses A ` ;

then not y in (A `) ^b by Th8;

hence x in ((A `) ^b) ` by SUBSET_1:29; :: thesis: verum