let x, y be ExtReal; :: thesis: for a, b being Real st x = a & y = b holds
x / y = a / b
let a, b be Real; :: thesis: ( x = a & y = b implies x / y = a / b )
assume A1: x = a ; :: thesis: ( not y = b or x / y = a / b )
assume y = b ; :: thesis: x / y = a / b
then y " = b " by XXREAL_3:def 6;
hence x / y = a / b by A1, XXREAL_3:def 5; :: thesis: verum