Tiny point: I think the comment in ltnsymd <http://us.metamath.org/mpegif/ltnsymd.html> could be improved. It says "'Less than' implies 'less than or equal to'." which is the same comment as the theorem before and I'm not sure it describes it. Maybe it should be "Less than implies not greater than." Unless I have misunderstood :)
-- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/e08dde21-bc70-4fa5-9d46-96dcc487890a%40googlegroups.com.
