let r be object ; :: thesis: ( r in REAL+ \ {0} iff r is positive Real )

hereby :: thesis: ( r is positive Real implies r in REAL+ \ {0} )

assume r in REAL+ \ {0} ; :: thesis: r is positive Real
then ( r in { r where r is Real : 0 <= r } & not r in {0} ) by REAL_1:1, XBOOLE_0:def 5;
then ( r <> 0 & ex s being Real st
( r = s & 0 <= s ) ) by TARSKI:def 1;
hence r is positive Real ; :: thesis: verum

end;

assume r is positive Real ; :: thesis: r in REAL+ \ {0}
then ( r in { r where r is Real : 0 <= r } & not r in {0} ) by TARSKI:def 1;
hence r in REAL+ \ {0} by REAL_1:1, XBOOLE_0:def 5; :: thesis: verum