set X = D1 "/\" D2;
let a, b be Element of L; :: according to WAYBEL_0:def 19 :: thesis: ( not a in D1 "/\" D2 or not b <= a or b in D1 "/\" D2 )
assume that
A1: a in D1 "/\" D2 and
A2: b <= a ; :: 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 11;
then x "/\" y <= x by LATTICE3:def 14;
then b <= x by A2, A3, YELLOW_0:def 2;
then A7: b in D1 by A4, WAYBEL_0:def 19;
x "/\" y <= y by A6, LATTICE3:def 14;
then b <= y by A2, A3, YELLOW_0:def 2;
then A8: b in D2 by A5, WAYBEL_0:def 19;
b = b "/\" b by YELLOW_0:25;
hence b in D1 "/\" D2 by A7, A8; :: thesis: verum