let L be transitive antisymmetric with_suprema RelStr ; :: thesis: for x, y, z being Element of L st x <= y holds
x "\/" z <= y "\/" z
let x, y, z be Element of L; :: thesis: ( x <= y implies x "\/" z <= y "\/" z )
assume A1: x <= y ; :: thesis: x "\/" z <= y "\/" z
y <= y "\/" z by YELLOW_0:22;
then ( x <= y "\/" z & z <= y "\/" z ) by A1, ORDERS_2:26, YELLOW_0:22;
hence x "\/" z <= y "\/" z by YELLOW_0:22; :: thesis: verum