let a be non trivial Nat; :: thesis: ex n being prime Nat st n divides a

per cases ( a is prime or not a is prime ) ;

suppose a is prime ; :: thesis: ex n being prime Nat st n divides a

hence ex n being prime Nat st n divides a ; :: thesis: verum

end;

suppose not a is prime ; :: thesis: ex n being prime Nat st n divides a

then ex n being Element of NAT st
( n > 1 & n * n <= a & n is prime & n divides a ) by NAT_4:14, Def0;
hence ex n being prime Nat st n divides a ; :: thesis: verum

end;

end;