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

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

for x being object holds

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

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

for x being object holds

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

proof

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

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

then reconsider y = x as Element of FT ;

U_FT y meets A by A4, Th8;

then ex z being object st

( z in U_FT y & z in A ) by XBOOLE_0:3;

then not U_FT y c= A ` by XBOOLE_0:def 5;

then not y in (A `) ^i by Th7;

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

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

proof

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

then reconsider y = x as Element of FT ;

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

then not U_FT y c= A ` ;

then consider z being object such that

A2: z in U_FT y and

A3: not z in A ` ;

z in A by A2, A3, SUBSET_1:29;

then U_FT y meets A by A2, XBOOLE_0:3;

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

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

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

then not U_FT y c= A ` ;

then consider z being object such that

A2: z in U_FT y and

A3: not z in A ` ;

z in A by A2, A3, SUBSET_1:29;

then U_FT y meets A by A2, XBOOLE_0:3;

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

then reconsider y = x as Element of FT ;

U_FT y meets A by A4, Th8;

then ex z being object st

( z in U_FT y & z in A ) by XBOOLE_0:3;

then not U_FT y c= A ` by XBOOLE_0:def 5;

then not y in (A `) ^i by Th7;

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