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