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