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 that
A1: a in D1 "\/" D2 and
A2: a <= b ; :: thesis: b in D1 "\/" D2
consider x, y being Element of L such that
A3: a = x "\/" y and
A4: x in D1 and
A5: y in D2 by A1;
A6: 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 by LATTICE3:def 13;
then x <= b by A2, A3, YELLOW_0:def 2;
then A7: b in D1 by A4, WAYBEL_0:def 20;
y <= x "\/" y by A6, LATTICE3:def 13;
then y <= b by A2, A3, YELLOW_0:def 2;
then A8: b in D2 by A5, WAYBEL_0:def 20;
b <= b ;
then b = b "\/" b by YELLOW_0:24;
hence b in D1 "\/" D2 by A7, A8; :: thesis: verum