theorem :: YELLOW_5:13

for L being transitive antisymmetric with_suprema with_infima RelStr
for a, b, c being Element of L st a <= b holds
a \ c <= b \ c by Th6;