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 object holds

( x in A ^delta iff x in (A ^deltai) \/ (A ^deltao) )

let A be Subset of FT; :: thesis: A ^delta = (A ^deltai) \/ (A ^deltao)

for x being object holds

( x in A ^delta iff x in (A ^deltai) \/ (A ^deltao) )

proof

hence
A ^delta = (A ^deltai) \/ (A ^deltao)
by TARSKI:2; :: thesis: verum
let x be object ; :: 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 )

then x in (A \/ (A `)) /\ (A ^delta) by XBOOLE_1:23;

then x in ([#] the carrier of FT) /\ (A ^delta) by SUBSET_1:10;

hence x in A ^delta by XBOOLE_1:28; :: thesis: verum

end;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 ^deltai) \/ (A ^deltao)
; :: thesis: x in A ^delta
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:10;

hence x in (A ^deltai) \/ (A ^deltao) by XBOOLE_1:23; :: thesis: verum

end;then x in ([#] the carrier of FT) /\ (A ^delta) by XBOOLE_1:28;

then x in (A \/ (A `)) /\ (A ^delta) by SUBSET_1:10;

hence x in (A ^deltai) \/ (A ^deltao) by XBOOLE_1:23; :: thesis: verum

then x in (A \/ (A `)) /\ (A ^delta) by XBOOLE_1:23;

then x in ([#] the carrier of FT) /\ (A ^delta) by SUBSET_1:10;

hence x in A ^delta by XBOOLE_1:28; :: thesis: verum