take {0,0,0} ; :: thesis: ex a, b, c being Element of NAT st
( (a ^2) + (b ^2) = c ^2 & {0,0,0} = {a,b,c} )
take 0 ; :: thesis: ex b, c being Element of NAT st
( (0 ^2) + (b ^2) = c ^2 & {0,0,0} = {0,b,c} )
take 0 ; :: thesis: ex c being Element of NAT st
( (0 ^2) + (0 ^2) = c ^2 & {0,0,0} = {0,0,c} )
take 0 ; :: thesis: ( (0 ^2) + (0 ^2) = 0 ^2 & {0,0,0} = {0,0,0} )
thus (0 ^2) + (0 ^2) = 0 ^2 ; :: thesis: {0,0,0} = {0,0,0}
thus {0,0,0} = {0,0,0} ; :: thesis: verum