let L be non empty join-commutative meet-commutative meet-associative meet-absorbing join-absorbing LattStr ; :: thesis: for x, y, z being Element of L st z [= x & z [= y & ( for z9 being Element of L st z9 [= x & z9 [= y holds
z9 [= z ) holds
z = x "/\" y
let x, y, z be Element of L; :: thesis: ( z [= x & z [= y & ( for z9 being Element of L st z9 [= x & z9 [= y holds
z9 [= z ) implies z = x "/\" y )
assume that
A1: ( z [= x & z [= y ) and
A2: for z9 being Element of L st z9 [= x & z9 [= y holds
z9 [= z ; :: thesis: z = x "/\" y
( x "/\" y [= x & x "/\" y [= y ) by LATTICES:6;
then A3: x "/\" y [= z by A2;
z [= x "/\" y by A1, Th7;
hence z = x "/\" y by A3, LATTICES:8; :: thesis: verum