∀H2:∀X:Univ.∀Y:Univ.eq Univ (join X Y) (join Y X).
∀H3:∀X:Univ.∀Y:Univ.eq Univ (meet X Y) (meet Y X).
∀H4:∀X:Univ.∀Y:Univ.eq Univ (join X (meet X Y)) X.
∀H2:∀X:Univ.∀Y:Univ.eq Univ (join X Y) (join Y X).
∀H3:∀X:Univ.∀Y:Univ.eq Univ (meet X Y) (meet Y X).
∀H4:∀X:Univ.∀Y:Univ.eq Univ (join X (meet X Y)) X.