defpred S1[ Nat] means <%x%>in A |^ $1; assume that A1:
<%x%>in A *and A2:
not <%x%>in A
; :: thesis: contradiction A3:
ex i being Nat st S1[i]
byA1, Th41;
ex n1 being Nat st ( S1[n1] & ( for n2 being Nat st S1[n2] holds n1 <= n2 ) )
fromNAT_1:sch 5(A3); then consider n1 being Nat such that A4:
S1[n1]
and A5:
for n2 being Nat st S1[n2] holds n1 <= n2
;