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

proof

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

proof

assume x in A ^delta ; :: thesis: x in (A ^deltai ) \/ (A ^deltao )
then x in ([#] the carrier of FT) /\ (A ^delta ) by XBOOLE_1:28;
then x in (A \/ (A ` )) /\ (A ^delta ) by SUBSET_1:25;
hence x in (A ^deltai ) \/ (A ^deltao ) by XBOOLE_1:23; :: thesis: verum

end;

assume x in (A ^deltai ) \/ (A ^deltao ) ; :: thesis: x in A ^delta
then x in (A \/ (A ` )) /\ (A ^delta ) by XBOOLE_1:23;
then x in ([#] the carrier of FT) /\ (A ^delta ) by SUBSET_1:25;
hence x in A ^delta by XBOOLE_1:28; :: thesis: verum

end;

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