for L being transitive antisymmetric with_suprema with_infima lower-bounded RelStr
for a, b, c being Element of L st a meets b \ c holds
a meets b