theorem Th20: :: SQUARE_1:20

sqrt 4 = 2 by Def2, Lm4;