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

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