let A1, A2 be Subset of NAT; :: thesis:
assume that
A1: for n being Nat holds
( n in A1 iff ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) ) ) and
A2: for n being Nat holds
( n in A2 iff ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) ) ) ; :: thesis:
for x being Element of NAT holds
( x in A1 iff x in A2 )

let x be Element of NAT ; :: thesis:
( x in A1 iff ( x is square-free & ( for i being Prime st i divides x holds
i <= p ) ) ) by A1;
hence ( x in A1 iff x in A2 ) by A2; :: thesis:

end;