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 that
A1: X is empty and
A2: not a ** X is empty ; :: thesis: contradiction
consider x being set such that
A3: x in a ** X by A2, XBOOLE_0:def 1;
ex y being Real st
( y in X & x = a * y ) by A3, Def2;
hence contradiction by A1; :: thesis: verum

end;

assume that
A4: a ** X is empty and
A5: not X is empty ; :: thesis: contradiction
consider x being set such that
A6: x in X by A5, XBOOLE_0:def 1;
reconsider x9 = x as Real by A6, XREAL_0:def 1;
a * x9 is Real ;
hence contradiction by A4, A6, Def2; :: thesis: verum