deffunc H₁( positive Nat) -> Subset of NAT = divisors ($1,4,1);
deffunc H₂( positive Nat) -> Subset of NAT = divisors ($1,4,3);
set X = { n where n is positive Nat : card H₁(n) > card H₂(n) } ;
set n = 5 |^ 0;
{ k where k is Nat : k divides 5 |^ 0 } = H₁(5 |^ 0) by Th36;
then A1: card H₁(5 |^ 0) = 0 + 1 by Th37;
card H₂(5 |^ 0) = 0 by Th38, CARD_1:27;
then A2: 5 |^ 0 in { n where n is positive Nat : card H₁(n) > card H₂(n) } by A1;
A3: { n where n is positive Nat : card H₁(n) > card H₂(n) } is natural-membered

let x be object ; :: according to MEMBERED:def 6 :: thesis:
assume x in { n where n is positive Nat : card H₁(n) > card H₂(n) } ; :: thesis:
then ex n being positive Nat st
( x = n & card H₁(n) > card H₂(n) ) ;
hence x is natural ; :: thesis:

end;

for a being Nat st a in { n where n is positive Nat : card H₁(n) > card H₂(n) } holds
ex b being Nat st
( b > a & b in { n where n is positive Nat : card H₁(n) > card H₂(n) } )

let a be Nat; :: thesis:
assume a in { n where n is positive Nat : card H₁(n) > card H₂(n) } ; :: thesis:
then consider n being positive Nat such that
A4: a = n and
card H₁(n) > card H₂(n) ;
take b = 5 |^ n; :: thesis:
thus b > a by A4, NEWTON:86; :: thesis:
A5: card H₂(b) = 0 by Th38, CARD_1:27;
{ k where k is Nat : k divides b } = H₁(b) by Th36;
then card H₁(b) = n + 1 by Th37;
hence b in { n where n is positive Nat : card H₁(n) > card H₂(n) } by A5; :: thesis:

end;