set X = [#] L;

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

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

assume that

x in [#] L and

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

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

ex z being Element of L st

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

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

hence ex z being Element of L st

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

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

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

assume that

x in [#] L and

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

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

ex z being Element of L st

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

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

hence ex z being Element of L st

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