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