( 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, Lm5, Lm6, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;
hence Real_Lattice is Lattice-like ; :: thesis: verum