∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (meet (meet (join X Y) (join Y Z)) Y) Y.
∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (join (join (meet X Y) (meet Y Z)) Y) Y.
∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (meet X (join Y (join X Z))) X.
∀H0:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (meet (meet (join X Y) (join Y Z)) Y) Y.
∀H1:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (join (join (meet X Y) (meet Y Z)) Y) Y.
∀H2:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (meet X (join Y (join X Z))) X.