theorem :: YELLOW_5:24

for L being transitive antisymmetric with_infima lower-bounded RelStr
for a, b, c being Element of L st a meets b & b <= c holds
a meets c