let X be real-membered set ; :: thesis: for a being real number holds
( X is empty iff a ** X is empty )
let a be real number ; :: thesis: ( X is empty iff a ** X is empty )
thus ( X is empty implies a ** X is empty ) :: thesis: ( a ** X is empty implies X is empty )

proof

assume A1: ( X is empty & not a ** X is empty ) ; :: thesis: contradiction
then consider x being set such that
A2: x in a ** X by XBOOLE_0:def 1;
consider y being Real such that
A3: ( y in X & x = a * y ) by A2, Def2;
thus contradiction by A1, A3; :: thesis: verum

end;

assume A4: ( a ** X is empty & not X is empty ) ; :: thesis: contradiction
then consider x being set such that
A5: x in X by XBOOLE_0:def 1;
x is real by A5;
then reconsider x' = x as Real by XREAL_0:def 1;
a * x' is Real ;
hence contradiction by A4, A5, Def2; :: thesis: verum