let a be real number ; :: thesis: ( 0 < a implies 0 < sqrt a )
assume 0 < a ; :: thesis: 0 < sqrt a
then ( sqrt a <> 0 ^2 & 0 <= sqrt a ) by Def4;
hence 0 < sqrt a ; :: thesis: verum