set X = D1 "\/" D2;
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 ) )
assume A1: ( a in D1 "\/" D2 & b in D1 "\/" D2 ) ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in D1 "\/" D2 & b₁ <= a & b₁ <= b )
then consider x, y being Element of L such that
A2: ( a = x "\/" y & x in D1 & y in D2 ) ;
consider s, t being Element of L such that
A3: ( b = s "\/" t & s in D1 & t in D2 ) by A1;
consider z1 being Element of L such that
A4: ( z1 in D1 & x >= z1 & s >= z1 ) by A2, A3, WAYBEL_0:def 2;
consider z2 being Element of L such that
A5: ( z2 in D2 & y >= z2 & t >= z2 ) by A2, A3, WAYBEL_0:def 2;
take z = z1 "\/" z2; :: thesis: ( z in D1 "\/" D2 & z <= a & z <= b )
thus z in D1 "\/" D2 by A4, A5; :: thesis: ( z <= a & z <= b )
thus ( z <= a & z <= b ) by A2, A3, A4, A5, YELLOW_3:3; :: thesis: verum