let n be non zero natural number ; :: thesis: { k where k is Element of NAT : ( 0 < k & k divides n & not k is square-containing ) } = { k where k is Element of NAT : ( 0 < k & k divides Radical n ) }
thus { k where k is Element of NAT : ( 0 < k & k divides n & not k is square-containing ) } c= { k where k is Element of NAT : ( 0 < k & k divides Radical n ) } :: according to XBOOLE_0:def 10 :: thesis: { k where k is Element of NAT : ( 0 < k & k divides Radical n ) } c= { k where k is Element of NAT : ( 0 < k & k divides n & not k is square-containing ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : ( 0 < k & k divides n & not k is square-containing ) } or x in { k where k is Element of NAT : ( 0 < k & k divides Radical n ) } )
assume x in { k where k is Element of NAT : ( 0 < k & k divides n & not k is square-containing ) } ; :: thesis: x in { k where k is Element of NAT : ( 0 < k & k divides Radical n ) }
then consider k1 being Element of NAT such that
A1: k1 = x and
A2: 0 < k1 and
A3: ( k1 divides n & not k1 is square-containing ) ;
k1 divides Radical n by A2, A3, Th65;
hence x in { k where k is Element of NAT : ( 0 < k & k divides Radical n ) } by A1, A2; :: thesis: verum

end;

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 ) } or x in { k where k is Element of NAT : ( 0 < k & k divides n & not k is square-containing ) } )
assume x in { k where k is Element of NAT : ( 0 < k & k divides Radical n ) } ; :: thesis: x in { k where k is Element of NAT : ( 0 < k & k divides n & not k is square-containing ) }
then consider k1 being Element of NAT such that
A4: ( x = k1 & 0 < k1 ) and
A5: k1 divides Radical n ;
A6: not k1 is square-containing by A5, Th26;
Radical n divides n by Th55;
then k1 divides n by A5, NAT_D:4;
hence x in { k where k is Element of NAT : ( 0 < k & k divides n & not k is square-containing ) } by A4, A6; :: thesis: verum