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 that
A1: xx in compactbelow x and
A2: 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;
yy is compact by A2, WAYBEL_8:4;
then ( yy <= xx "\/" yy & yy << yy ) by YELLOW_0:22;
then A3: yy << xx "\/" yy by WAYBEL_3:2;
xx is compact by A1, WAYBEL_8:4;
then ( xx <= xx "\/" yy & xx << xx ) by YELLOW_0:22;
then xx << xx "\/" yy by WAYBEL_3:2;
then xx "\/" yy << xx "\/" yy by A3, WAYBEL_3:3;
then A4: xx "\/" yy is compact ;
take xx "\/" yy ; :: thesis: ( xx "\/" yy in compactbelow x & xx <= xx "\/" yy & yy <= xx "\/" yy )
( xx <= x & yy <= x ) by A1, A2, WAYBEL_8:4;
then xx "\/" yy <= x by YELLOW_0:22;
hence xx "\/" yy in compactbelow x by A4; :: thesis: ( xx <= xx "\/" yy & yy <= xx "\/" yy )
thus ( xx <= xx "\/" yy & yy <= xx "\/" yy ) by YELLOW_0:22; :: thesis: verum