not (min (a,b)) / (max (a,b)) is heavy ;
then not ((max (a,b)) / (min (a,b))) " is heavy by XCMPLX_1:213;
hence not (max (a,b)) / (min (a,b)) is light ; :: thesis: verum