let a, b be Element of L; WAYBEL_0:def 1 ( 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 & a <= b1 & b <= b1 ) )
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 & a <= b1 & b <= b1 )
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 1;
consider z1 being Element of L such that
A11:
z1 in D1
and
A12:
( x <= z1 & s <= z1 )
by A4, A7, WAYBEL_0:def 1;
take z = z1 "/\" z2; ( z in D1 "/\" D2 & a <= z & b <= z )
thus
z in D1 "/\" D2
by A11, A9; ( a <= z & b <= z )
thus
( a <= z & b <= z )
by A3, A6, A12, A10, YELLOW_3:2; verum