let h be Integer; :: thesis: ( h <> 0 implies PrimeDivisors>3 h c= Seg |.h.| )
assume A1: h <> 0 ; :: thesis: PrimeDivisors>3 h c= Seg |.h.|
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PrimeDivisors>3 h or x in Seg |.h.| )
assume A2: x in PrimeDivisors>3 h ; :: thesis: x in Seg |.h.|
then reconsider x = x as Element of NAT ;
A3: x >= 1 by A2, Th35, XXREAL_0:2;
x divides h by A2, Th36;
then x <= |.h.| by A1, Th4, NAT_D:7;
hence x in Seg |.h.| by A3; :: thesis: verum