let L be transitive antisymmetric with_suprema RelStr ; :: thesis: for a, b, c, d being Element of L st a <= c & b <= d holds
a "\/" b <= c "\/" d
let a, b, c, d be Element of L; :: thesis: ( a <= c & b <= d implies a "\/" b <= c "\/" d )
assume that
A1: a <= c and
A2: b <= d ; :: thesis: a "\/" b <= c "\/" d
A3: ex_sup_of {c,d},L by YELLOW_0:20;
then d <= c "\/" d by YELLOW_0:18;
then A4: b <= c "\/" d by A2, ORDERS_2:3;
c <= c "\/" d by A3, YELLOW_0:18;
then ( ex x being Element of L st
( a <= x & b <= x & ( for z being Element of L st a <= z & b <= z holds
x <= z ) ) & a <= c "\/" d ) by A1, LATTICE3:def 10, ORDERS_2:3;
hence a "\/" b <= c "\/" d by A4, LATTICE3:def 13; :: thesis: verum