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

per cases ( a < b or b < a ) by A1, 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;