let A be Subset of REAL; :: thesis: ( A <> {} implies 0 ** A = {0} )
assume A1: A <> {} ; :: thesis: 0 ** A = {0}
A2: {0} c= 0 ** A

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {0} or y in 0 ** A )
consider t being object such that
A3: t in A by A1, XBOOLE_0:def 1;
reconsider t = t as Element of A by A3;
reconsider t = t as Real ;
assume y in {0} ; :: thesis: y in 0 ** A
then y = 0 * t by TARSKI:def 1;
hence y in 0 ** A by A3, MEMBER_1:193; :: thesis: verum

end;

0 ** A c= {0}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in 0 ** A or y in {0} )
assume A4: y in 0 ** A ; :: thesis: y in {0}
then reconsider y = y as Real ;
ex z being Real st
( z in A & y = 0 * z ) by A4, INTEGRA2:39;
hence y in {0} by TARSKI:def 1; :: thesis: verum

end;

hence 0 ** A = {0} by A2; :: thesis: verum