let a, b be Element of L; WAYBEL_0:def 2 ( not a in D1 "/\" D2 or not b in D1 "/\" D2 or ex b1 being Element of the carrier of L st
( b1 in D1 "/\" D2 & b1 <= a & b1 <= b ) )
set X = D1 "/\" D2;
assume that
A1:
a in D1 "/\" D2
and
A2:
b in D1 "/\" D2
; ex b1 being Element of the carrier of L st
( b1 in D1 "/\" D2 & b1 <= a & b1 <= b )
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;
consider s, t being Element of L such that
A6:
b = s "/\" t
and
A7:
s in D1
and
A8:
t in D2
by A2;
consider z2 being Element of L such that
A9:
z2 in D2
and
A10:
( y >= z2 & t >= z2 )
by A5, A8, WAYBEL_0:def 2;
consider z1 being Element of L such that
A11:
z1 in D1
and
A12:
( x >= z1 & s >= z1 )
by A4, A7, WAYBEL_0:def 2;
take z = z1 "/\" z2; ( z in D1 "/\" D2 & z <= a & z <= b )
thus
z in D1 "/\" D2
by A11, A9; ( z <= a & z <= b )
thus
( z <= a & z <= b )
by A3, A6, A12, A10, YELLOW_3:2; verum