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