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 z' being Element of L st z' [= x & z' [= y holds
z' [= z ) holds
z = x "/\" y
let x, y, z be Element of L; :: thesis: ( z [= x & z [= y & ( for z' being Element of L st z' [= x & z' [= y holds
z' [= z ) implies z = x "/\" y )
assume that
A1: z [= x and
A2: z [= y and
A3: for z' being Element of L st z' [= x & z' [= y holds
z' [= z ; :: thesis: z = x "/\" y
A4: z [= x "/\" y by A1, A2, Th7;
( x "/\" y [= x & x "/\" y [= y ) by LATTICES:23;
then x "/\" y [= z by A3;
hence z = x "/\" y by A4, LATTICES:26; :: thesis: verum