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

proof

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

end;

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

proof

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

end;