let a, b be Real; :: thesis: ( not a <> b or 0 < a - b or 0 < b - a )
assume a <> b ; :: thesis: ( 0 < a - b or 0 < b - a )

per cases then ( a < b or b < a ) by XXREAL_0:1;

suppose a < b ; :: thesis: ( 0 < a - b or 0 < b - a )

then 0 + a < b ;
hence ( 0 < a - b or 0 < b - a ) by Lm19; :: thesis: verum

end;

suppose b < a ; :: thesis: ( 0 < a - b or 0 < b - a )

then 0 + b < a ;
hence ( 0 < a - b or 0 < b - a ) by Lm19; :: thesis: verum

end;

end;