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

proof

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

proof

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

end;

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

end;

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