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