let L be transitive antisymmetric with_suprema RelStr ; :: thesis: for a, b being Element of L
for A, B being Subset of L st a is_>=_than A & b is_>=_than B holds
a "\/" b is_>=_than A "\/" B
let a, b be Element of L; :: thesis: for A, B being Subset of L st a is_>=_than A & b is_>=_than B holds
a "\/" b is_>=_than A "\/" B
let A, B be Subset of L; :: thesis: ( a is_>=_than A & b is_>=_than B implies a "\/" b is_>=_than A "\/" B )
assume A1: ( a is_>=_than A & b is_>=_than B ) ; :: thesis: a "\/" b is_>=_than A "\/" B
let q be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not q in A "\/" B or q <= a "\/" b )
assume q in A "\/" B ; :: thesis: q <= a "\/" b
then consider x, y being Element of L such that
A2: q = x "\/" y and
A3: ( x in A & y in B ) ;
( a >= x & b >= y ) by A1, A3;
hence q <= a "\/" b by A2, YELLOW_3:3; :: thesis: verum