let n be non zero Element of NAT ; :: thesis: for p being Prime holds { k where k is Element of NAT : ( 0 < k & k divides Radical n & p divides k ) } c= Seg n
let p be Prime; :: thesis: { k where k is Element of NAT : ( 0 < k & k divides Radical n & p divides k ) } c= Seg n
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : ( 0 < k & k divides Radical n & p divides k ) } or x in Seg n )
assume x in { k where k is Element of NAT : ( 0 < k & k divides Radical n & p divides k ) } ; :: thesis: x in Seg n
then consider k being Element of NAT such that
A1: x = k and
A2: k > 0 and
A3: k divides Radical n and
p divides k ;
A4: 1 <= k by A2, NAT_1:14;
A5: Radical n <= n by Th55, NAT_D:7;
k <= Radical n by A3, NAT_D:7;
then k <= n by A5, XXREAL_0:2;
hence x in Seg n by A1, A4, FINSEQ_1:1; :: thesis: verum