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 A1: ( a <= c & b <= d ) ; :: thesis: a "\/" b <= c "\/" d
A2: 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 ) ) by LATTICE3:def 10;
ex_sup_of {c,d},L by YELLOW_0:20;
then ( c <= c "\/" d & d <= c "\/" d ) by YELLOW_0:18;
then ( a <= c "\/" d & b <= c "\/" d ) by A1, ORDERS_2:26;
hence a "\/" b <= c "\/" d by A2, LATTICE3:def 13; :: thesis: verum