let a, b be Element of L; :: according to WAYBEL_0:def 2 :: thesis: ( not a in D1 "\/" D2 or not b in D1 "\/" D2 or ex b₁ being Element of the carrier of L st
( b₁ in D1 "\/" D2 & b₁ <= a & b₁ <= b ) )
set X = D1 "\/" D2;
assume that
A1: a in D1 "\/" D2 and
A2: b in D1 "\/" D2 ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in D1 "\/" D2 & b₁ <= a & b₁ <= 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; :: thesis: ( z in D1 "\/" D2 & z <= a & z <= b )
thus z in D1 "\/" D2 by A11, A9; :: thesis: ( z <= a & z <= b )
thus ( z <= a & z <= b ) by A3, A6, A12, A10, YELLOW_3:3; :: thesis: verum