Identify

without 'when' statement

registration
  let p, q be Element of Nat_Lattice;
  identify p "\/" q with p lcm q;
  compatibility
  proof
    thus p "\/" q = p lcm q;
  end;
end;

with 'when' statement

registration
  let a be Element of G_Real, x be real number;
  identify -a with -x when a = x;
  compatibility
  proof
    thus a = x implies -a = -x;
  end;
end;