let x, y be real number ; :: thesis: ( y > 0 implies (min x,y) / (max x,y) <= 1 )
assume A1: y > 0 ; :: thesis: (min x,y) / (max x,y) <= 1

per cases ( x > 0 or x <= 0 ) ;

suppose A2: x > 0 ; :: thesis: (min x,y) / (max x,y) <= 1

now

per cases ( x >= y or x < y ) ;

suppose A3: x >= y ; :: thesis: (min x,y) / (max x,y) <= 1

then ( max x,y = x & min x,y = y ) by XXREAL_0:def 9, XXREAL_0:def 10;
hence (min x,y) / (max x,y) <= 1 by A1, A3, XREAL_1:185; :: thesis: verum

end;

suppose A4: x < y ; :: thesis: (min x,y) / (max x,y) <= 1

then ( max x,y = y & min x,y = x ) by XXREAL_0:def 9, XXREAL_0:def 10;
hence (min x,y) / (max x,y) <= 1 by A2, A4, XREAL_1:185; :: thesis: verum

end;

end;

end;

hence (min x,y) / (max x,y) <= 1 ; :: thesis: verum

end;

suppose A5: x <= 0 ; :: thesis: (min x,y) / (max x,y) <= 1

then ( min x,y = x & max x,y = y ) by A1, XXREAL_0:def 9, XXREAL_0:def 10;
hence (min x,y) / (max x,y) <= 1 by A1, A5; :: thesis: verum

end;

end;