let X be Tolerance_Space; :: thesis: for A, B being RoughSet of X holds UAp (A _\/_ B) = (UAp A) \/ (UAp B)
let A, B be RoughSet of X; :: thesis: UAp (A _\/_ B) = (UAp A) \/ (UAp B)
thus UAp (A _\/_ B) c= (UAp A) \/ (UAp B) :: according to XBOOLE_0:def 10 :: thesis: (UAp A) \/ (UAp B) c= UAp (A _\/_ B)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in UAp (A _\/_ B) or x in (UAp A) \/ (UAp B) )
assume x in UAp (A _\/_ B) ; :: thesis: x in (UAp A) \/ (UAp B)
hence x in (UAp A) \/ (UAp B) by MCART_1:7; :: thesis: verum

end;

thus (UAp A) \/ (UAp B) c= UAp (A _\/_ B) :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (UAp A) \/ (UAp B) or x in UAp (A _\/_ B) )
assume x in (UAp A) \/ (UAp B) ; :: thesis: x in UAp (A _\/_ B)
hence x in UAp (A _\/_ B) by MCART_1:7; :: thesis: verum

end;