dist (|[0,0]|,|[1,0]|) = sqrt (((0 - 1) ^2) + ((0 - 0) ^2)) by THYQ
.= sqrt (((- 1) * (- 1)) + (0 ^2)) by SQUARE_1:def 1
.= sqrt (1 + (0 * 0)) by SQUARE_1:def 1
.= 1 by SQUARE_1:18 ;
hence dist (|[0,0]|,|[1,0]|) = 1 ; :: thesis: verum