let a be Real; :: thesis: ( 0 < a implies 0 < sqrt a )
assume A1: 0 < a ; :: thesis: 0 < sqrt a
then sqrt a <> 0 ^2 by Def2;
hence 0 < sqrt a by A1, Def2; :: thesis: verum