let L be WA_Lattice; :: thesis: for x, y being Element of L ex z being Element of L st
( z [= x & z [= y & ( for u being Element of L st u [= x & u [= y holds
u [= z ) )
let x, y be Element of L; :: thesis: ex z being Element of L st
( z [= x & z [= y & ( for u being Element of L st u [= x & u [= y holds
u [= z ) )
take z = x "/\" y; :: thesis: ( z [= x & z [= y & ( for u being Element of L st u [= x & u [= y holds
u [= z ) )
thus ( z [= x & z [= y & ( for u being Element of L st u [= x & u [= y holds
u [= z ) ) by Lemacik2, Lemacik3; :: thesis: verum