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 )
proof
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) ` )
proof
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 ;
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 ;
then U_FT y meets A by ;
hence x in A ^b ; :: thesis: verum
end;
assume A4: x in A ^b ; :: thesis: x in ((A `) ^i) `
then reconsider y = x as Element of FT ;
U_FT y meets A by ;
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;
hence ((A `) ^i) ` = A ^b by TARSKI:2; :: thesis: verum