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