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

proof

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

proof

assume A1: x in A ^delta ; :: thesis: x in (A ^b ) /\ ((A ^i ) ` )
then reconsider y = x as Element of FT ;
U_FT y meets A ` by A1, FIN_TOPO:10;
then y in (((A ` ) ^b ) ` ) ` ;
then A2: y in (A ^i ) ` by FIN_TOPO:23;
U_FT y meets A by A1, FIN_TOPO:10;
then y in A ^b ;
hence x in (A ^b ) /\ ((A ^i ) ` ) by A2, XBOOLE_0:def 4; :: thesis: verum

end;

assume A3: x in (A ^b ) /\ ((A ^i ) ` ) ; :: thesis: x in A ^delta
then reconsider y = x as Element of FT ;
x in (A ^i ) ` by A3, XBOOLE_0:def 4;
then x in (((A ` ) ^b ) ` ) ` by FIN_TOPO:23;
then A4: U_FT y meets A ` by FIN_TOPO:13;
x in A ^b by A3, XBOOLE_0:def 4;
then U_FT y meets A by FIN_TOPO:13;
hence x in A ^delta by A4; :: thesis: verum

end;

hence A ^delta = (A ^b ) /\ ((A ^i ) ` ) by TARSKI:2; :: thesis: verum