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