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 that
A1: u1 in AR -below x and
A2: 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₁ )
A3: ex v1 being Element of L st
( v1 = u1 & [v1,x] in AR ) by A1;
A4: ex v2 being Element of L st
( v2 = u2 & [v2,x] in AR ) by A2;
take u12 = u1 "\/" u2; :: thesis: ( u12 in AR -below x & u1 <= u12 & u2 <= u12 )
[u12,x] in AR by A3, A4, Def5;
hence ( u12 in AR -below x & u1 <= u12 & u2 <= u12 ) by YELLOW_0:22; :: thesis: verum