let a, b be Element of L; :: according to WAYBEL_0:def 1 :: 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 & a <= b₁ & 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 & a <= b₁ & 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 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; :: thesis: ( z in D1 "\/" D2 & a <= z & b <= z )
thus z in D1 "\/" D2 by A11, A9; :: thesis: ( a <= z & b <= z )
thus ( a <= z & b <= z ) by A3, A6, A12, A10, YELLOW_3:3; :: thesis: verum