# Exercise 8.8

Leaving aside the argument about axioms by definition not requiring proof…

Axiom 3:

```(r1 `Intersect` (r2 `Union` r3)) `containsR` p
=> (r1 `containsR` p) && ((r2 `Union` r3) `containsR` p)
=> (r1 `containsR` p) && ((r2 `containsR` p) || (r3 `containsR` p))
=> ((r1 `containsR` p) && (r2 `containsR` p))
|| ((r1 `containsR` p) && (r3 `containsR` p))
=> ((r1 `Intersect` r2) `containsR` p) || ((r1 `Intersect` r3) `containsR` p)
=> ((r1 `Intersect` r2) `Union` (r1 `Intersect` r3)) `containsR` p

âˆ´ (r1 `Intersect` (r2 `Union` r3))
â‰¡ ((r1 `Intersect` r2) `Union` (r1 `Intersect` r3))

(r1 `Union` (r2 `Intersect` r3)) `containsR` p
=> (r1 `containsR` p) || ((r2 `Intersect` r3) `containsR` p)
=> (r1 `containsR` p) || ((r2 `containsR` p) && (r3 `containsR` p))
=> ((r1 `containsR` p) || (r2 `containsR` p))
&& ((r1 `containsR` p) || (r3 `containsR` p))
=> ((r1 `Union` r2) `containsR` p) && ((r1 `Union` r3) `containsR` p)
=> ((r1 `Union` r2) `Intersect` (r1 `Union` r3)) `containsR` p

âˆ´ (r1 `Union` (r2 `Intersect` r3))
â‰¡ ((r1 `Union` r2) `Intersect` (r1 `Union` r3))```

Axiom 4:

```univ = Complement Empty

(r `Union` Empty) `containsR` p
=> (r `containsR` p) || (Empty `containsR` p)
=> (r `containsR` p) || False
=> r `containsR` p

âˆ´ (r `Union` Empty) â‰¡ r

(r `Intersect` univ) `containsR` p
=> (r `Intersect` Complement Empty) `containsR` p
=> (r `containsR` p) && (Complement Empty `containsR` p)
=> (r `containsR` p) && not (Empty `containsR` p)
=> (r `containsR` p) && not False
=> (r `containsR` p) && True
=> r `containsR` p

âˆ´ (r `Intersect` univ) â‰¡ r```

Axiom 5:

```(r `Union` Complement r) `containsR` p
=> (r `containsR` p) || (Complement r `containsR` p)
=> (r `containsR` p) || not (r `containsR` p)
=> True
=> not False
=> not (Empty `containsR` p)
=> Complement Empty `containsR` p
=> univ `containsR` p

âˆ´ (r `Union` Complement r) â‰¡ univ

(r `Intersect` Complement r) `containsR` p
=> (r `containsR` p) && (Complement r `containsR` p)
=> (r `containsR` p) && not (r `containsR` p)
=> False
=> Empty `containsR` p

âˆ´ (r `Intersect` Complement r) â‰¡ Empty```