let n be Nat; :: thesis: succ n = { l where l is Element of NAT : l <= n }
defpred S₁[ Nat] means $1 <= n;
defpred S₂[ Nat] means $1 < n + 1;
deffunc H₁( Nat) -> Nat = $1;
A1: for l being Element of NAT holds
( S₂[l] iff S₁[l] ) by Th13;
thus succ n = n + 1
.= { H₁(l) where l is Element of NAT : S₂[l] } by AXIOMS:4
.= { H₁(l) where l is Element of NAT : S₁[l] } from FRAENKEL:sch 3(A1) ; :: thesis: verum