let L be non empty transitive antisymmetric with_suprema RelStr ; :: thesis: for a, b, c being Element of L st a <= b holds
a "\/" c <= b "\/" c
let a, b, c be Element of L; :: thesis: ( a <= b implies a "\/" c <= b "\/" c )
A1: b <= b "\/" c by YELLOW_0:22;
A2: c <= b "\/" c by YELLOW_0:22;
assume a <= b ; :: thesis: a "\/" c <= b "\/" c
then a <= b "\/" c by A1, YELLOW_0:def 2;
hence a "\/" c <= b "\/" c by A2, YELLOW_0:22; :: thesis: verum