assume
[x,y] is natural
; contradiction
then reconsider n = [x,y] as Nat ;
card n <= 2
by Th49;
then
n <= 2
;
then
not not n = 0 & ... & not n = 2
;
per cases then
( n = 0 or n = 1 or n = 2 )
;
suppose
n = 0
;
contradictionhence
contradiction
;
verum end; end;