set cX = compactbelow x;
let xx, yy be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( not xx in compactbelow x or not yy in compactbelow x or ex b₁ being Element of the carrier of L st
( b₁ in compactbelow x & xx <= b₁ & yy <= b₁ ) )
assume A1: ( xx in compactbelow x & yy in compactbelow x ) ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in compactbelow x & xx <= b₁ & yy <= b₁ )
set z = xx "\/" yy;
take xx "\/" yy ; :: thesis: ( xx "\/" yy in compactbelow x & xx <= xx "\/" yy & yy <= xx "\/" yy )
( xx <= x & yy <= x ) by A1, WAYBEL_8:4;
then A2: xx "\/" yy <= x by YELLOW_0:22;
A3: ( xx <= xx "\/" yy & yy <= xx "\/" yy ) by YELLOW_0:22;
( xx is compact & yy is compact ) by A1, WAYBEL_8:4;
then ( xx << xx & yy << yy ) by WAYBEL_3:def 2;
then ( xx << xx "\/" yy & yy << xx "\/" yy ) by A3, WAYBEL_3:2;
then xx "\/" yy << xx "\/" yy by WAYBEL_3:3;
then xx "\/" yy is compact by WAYBEL_3:def 2;
hence xx "\/" yy in compactbelow x by A2; :: thesis: ( xx <= xx "\/" yy & yy <= xx "\/" yy )
thus ( xx <= xx "\/" yy & yy <= xx "\/" yy ) by YELLOW_0:22; :: thesis: verum