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