set I = AR -below x;
let u1, u2 be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( not u1 in AR -below x or not u2 in AR -below x or ex b₁ being Element of the carrier of L st
( b₁ in AR -below x & u1 <= b₁ & u2 <= b₁ ) )
assume A1: ( u1 in AR -below x & u2 in AR -below x ) ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in AR -below x & u1 <= b₁ & u2 <= b₁ )
then consider v1 being Element of L such that
A2: ( v1 = u1 & [v1,x] in AR ) ;
consider v2 being Element of L such that
A3: ( v2 = u2 & [v2,x] in AR ) by A1;
take u12 = u1 "\/" u2; :: thesis: ( u12 in AR -below x & u1 <= u12 & u2 <= u12 )
[u12,x] in AR by A2, A3, Def6;
hence ( u12 in AR -below x & u1 <= u12 & u2 <= u12 ) by YELLOW_0:22; :: thesis: verum