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 ( x in [#] L & 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 z' being Element of L st z' <= x & z' <= y holds
z' <= z ) ) by LATTICE3:def 11;
hence ex z being Element of L st
( z in [#] L & z <= x & z <= y ) ; :: thesis: verum