take |.h.| ; :: according to FINSEQ_1:def 13 :: thesis: PrimeDivisors>3 h c= Seg |.h.|
thus PrimeDivisors>3 h c= Seg |.h.| by Th39; :: thesis: verum