let A1, A2 be Subset of NAT; :: thesis: ( ( for n being Nat holds
( n in A1 iff ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) ) ) ) & ( for n being Nat holds
( n in A2 iff ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) ) ) ) implies A1 = A2 )
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: A1 = A2
for x being Element of NAT holds
( x in A1 iff x in A2 )

proof

let x be Element of NAT ; :: thesis: ( x in A1 iff x in A2 )
( 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: verum

end;

hence A1 = A2 by SUBSET_1:3; :: thesis: verum