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
reconsider XX = X as empty set by A1;
a ** XX is empty ;
hence contradiction by A2; :: 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;
thus contradiction by A4, A6; :: thesis: verum