set X = D1 "\/" D2;
let a, b be Element of L; :: according to WAYBEL_0:def 20 :: thesis: ( not a in D1 "\/" D2 or not a <= b or b in D1 "\/" D2 )
assume A1: ( a in D1 "\/" D2 & a <= b ) ; :: thesis: b in D1 "\/" D2
consider x, y being Element of L such that
A2: ( a = x "\/" y & x in D1 & y in D2 ) by A1;
ex xx being Element of L st
( x <= xx & y <= xx & ( for c being Element of L st x <= c & y <= c holds
xx <= c ) ) by LATTICE3:def 10;
then ( x <= x "\/" y & y <= x "\/" y ) by LATTICE3:def 13;
then ( x <= b & y <= b ) by A1, A2, YELLOW_0:def 2;
then A3: ( b in D1 & b in D2 ) by A2, WAYBEL_0:def 20;
b <= b ;
then b = b "\/" b by YELLOW_0:24;
hence b in D1 "\/" D2 by A3; :: thesis: verum