let y, z be Real; :: thesis: ( y - z <> 0 implies sinh ((y / 2) - (z / 2)) <> 0 )
assume y - z <> 0 ; :: thesis: sinh ((y / 2) - (z / 2)) <> 0
then (y - z) / 2 <> 0 ;
hence sinh ((y / 2) - (z / 2)) <> 0 by Lm4; :: thesis: verum