theorem :: YELLOW_5:29

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