let a be Real; :: thesis: ( ( not a is light & a is negative implies a <= - 1 ) & ( a <= - 1 implies ( not a is light & a is negative ) ) & ( not a is heavy & a is negative implies ( - 1 <= a & a < 0 ) ) & ( - 1 <= a & a < 0 implies ( not a is heavy & a is negative ) ) & ( not a is heavy & a is positive implies ( 0 < a & a <= 1 ) ) & ( 0 < a & a <= 1 implies ( not a is heavy & a is positive ) ) & ( not a is light & a is positive implies 1 <= a ) & ( 1 <= a implies ( not a is light & a is positive ) ) )
A1: ( not a is light & a is negative implies a <= - 1 )
proof
assume ( not a is light & a is negative ) ; :: thesis: a <= - 1
then - a >= 1 by ABSVALUE:def 1;
then - (- a) <= - 1 by XREAL_1:24;
hence a <= - 1 ; :: thesis: verum
end;
A1a: ( a <= - 1 implies ( not a is light & a is negative ) )
proof
assume B1: a <= - 1 ; :: thesis: ( not a is light & a is negative )
then - a >= - (- 1) by XREAL_1:24;
hence ( not a is light & a is negative ) by B1, ABSVALUE:def 1; :: thesis: verum
end;
A3: ( not a is heavy & a is negative implies ( - 1 <= a & a < 0 ) )
proof
assume B1: ( not a is heavy & a is negative ) ; :: thesis: ( - 1 <= a & a < 0 )
then - a <= 1 by ABSVALUE:def 1;
then - (- a) >= - 1 by XREAL_1:24;
hence ( - 1 <= a & a < 0 ) by B1; :: thesis: verum
end;
( - 1 <= a & a < 0 implies ( not a is heavy & a is negative ) )
proof
assume B1: ( - 1 <= a & a < 0 ) ; :: thesis: ( not a is heavy & a is negative )
then - a <= - (- 1) by XREAL_1:24;
hence ( not a is heavy & a is negative ) by B1, ABSVALUE:def 1; :: thesis: verum
end;
hence ( ( not a is light & a is negative implies a <= - 1 ) & ( a <= - 1 implies ( not a is light & a is negative ) ) & ( not a is heavy & a is negative implies ( - 1 <= a & a < 0 ) ) & ( - 1 <= a & a < 0 implies ( not a is heavy & a is negative ) ) & ( not a is heavy & a is positive implies ( 0 < a & a <= 1 ) ) & ( 0 < a & a <= 1 implies ( not a is heavy & a is positive ) ) & ( not a is light & a is positive implies 1 <= a ) & ( 1 <= a implies ( not a is light & a is positive ) ) ) by A1, A1a, A3; :: thesis: verum