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 & not p divides k ) } c= Seg n
let p be Prime; :: thesis: { k where k is Element of NAT : ( 0 < k & k divides Radical n & not p divides k ) } c= Seg n
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : ( 0 < k & k divides Radical n & not p divides k ) } or x in Seg n )
assume x in { k where k is Element of NAT : ( 0 < k & k divides Radical n & not p divides k ) } ; :: thesis: x in Seg n
then consider k being Element of NAT such that
A1: ( x = k & k > 0 & k divides Radical n & not p divides k ) ;
( k <= Radical n & Radical n <= n ) by A1, Th55, NAT_D:7;
then ( 1 <= k & k <= n ) by A1, NAT_1:14, XXREAL_0:2;
hence x in Seg n by A1, FINSEQ_1:3; :: thesis: verum