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 8 :: thesis: ( not q in A "\/" B or a "\/" b <= q )
assume q in A "\/" B ; :: thesis: a "\/" b <= q
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 a "\/" b <= q by A2, YELLOW_3:3; :: thesis: verum