let v, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( not v in waybelow x or not y in waybelow x or ex b₁ being Element of the carrier of L st
( b₁ in waybelow x & v <= b₁ & y <= b₁ ) )
assume that
A1: v in waybelow x and
A2: y in waybelow x ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in waybelow x & v <= b₁ & y <= b₁ )
A3: v << x by A1, Th7;
A4: y << x by A2, Th7;
then A5: ex_sup_of {v,y},L by A3, Th3;
take z = v "\/" y; :: thesis: ( z in waybelow x & v <= z & y <= z )
z << x by A3, A4, Th3;
hence z in waybelow x ; :: thesis: ( v <= z & y <= z )
thus ( v <= z & y <= z ) by A5, YELLOW_0:18; :: thesis: verum