set X = D1 "/\" D2;
let a, b be Element of L; WAYBEL_0:def 19 ( 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
; 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; verum