let X be Tolerance_Space; :: thesis: for A, B being RoughSet of X holds A _/\_ (A _\/_ B) = A

let A, B be RoughSet of X; :: thesis: A _/\_ (A _\/_ B) = A

A1: LAp (A _/\_ (A _\/_ B)) = (LAp A) /\ (LAp (A _\/_ B))

.= (LAp A) /\ ((LAp A) \/ (LAp B))

.= LAp A by XBOOLE_1:21 ;

UAp (A _/\_ (A _\/_ B)) = (UAp A) /\ (UAp (A _\/_ B))

.= (UAp A) /\ ((UAp A) \/ (UAp B))

.= UAp A by XBOOLE_1:21 ;

hence A _/\_ (A _\/_ B) = A by A1; :: thesis: verum

let A, B be RoughSet of X; :: thesis: A _/\_ (A _\/_ B) = A

A1: LAp (A _/\_ (A _\/_ B)) = (LAp A) /\ (LAp (A _\/_ B))

.= (LAp A) /\ ((LAp A) \/ (LAp B))

.= LAp A by XBOOLE_1:21 ;

UAp (A _/\_ (A _\/_ B)) = (UAp A) /\ (UAp (A _\/_ B))

.= (UAp A) /\ ((UAp A) \/ (UAp B))

.= UAp A by XBOOLE_1:21 ;

hence A _/\_ (A _\/_ B) = A by A1; :: thesis: verum