theorem :: YELLOW_5:30

for L being transitive antisymmetric with_infima lower-bounded RelStr
for a, b, c being Element of L st ( a misses b or a misses c ) holds
a misses b "/\" c