( Real_Lattice is join-commutative & Real_Lattice is join-associative & Real_Lattice is meet-absorbing & Real_Lattice is meet-commutative & Real_Lattice is meet-associative & Real_Lattice is join-absorbing )
by Lm1, Lm2, Lm3, Lm4;
hence
Real_Lattice is Lattice-like
; verum