set X = [#] L;

let x, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( x in [#] L & y in [#] L implies ex z being Element of L st

( z in [#] L & x <= z & y <= z ) )

assume that

x in [#] L and

y in [#] L ; :: thesis: ex z being Element of L st

( z in [#] L & x <= z & y <= z )

ex z being Element of L st

( x <= z & y <= z & ( for z9 being Element of L st x <= z9 & y <= z9 holds

z <= z9 ) ) by LATTICE3:def 10;

hence ex z being Element of L st

( z in [#] L & x <= z & y <= z ) ; :: thesis: verum

let x, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( x in [#] L & y in [#] L implies ex z being Element of L st

( z in [#] L & x <= z & y <= z ) )

assume that

x in [#] L and

y in [#] L ; :: thesis: ex z being Element of L st

( z in [#] L & x <= z & y <= z )

ex z being Element of L st

( x <= z & y <= z & ( for z9 being Element of L st x <= z9 & y <= z9 holds

z <= z9 ) ) by LATTICE3:def 10;

hence ex z being Element of L st

( z in [#] L & x <= z & y <= z ) ; :: thesis: verum