0 <> 1 ;
hence ex a, b being Element of G_Real st a <> b ; :: thesis: verum