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
A3: a ** X is empty and
A4: not X is empty ; :: thesis: contradiction
consider x being set such that
A5: x in X by A4, XBOOLE_0:def 1;
thus contradiction by A3, A5; :: thesis: verum