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 )
A1: y <= y "\/" z by YELLOW_0:22;
A2: z <= y "\/" z by YELLOW_0:22;
assume x <= y ; :: thesis: x "\/" z <= y "\/" z
then x <= y "\/" z by A1, ORDERS_2:3;
hence x "\/" z <= y "\/" z by A2, YELLOW_0:22; :: thesis: verum