let s1, s2 be Subset of NAT; :: thesis: ( ( for n being Nat holds
( n in s1 iff ex k being Nat st
( n = (4 * k) + 3 & n is prime ) ) ) & ( for n being Nat holds
( n in s2 iff ex k being Nat st
( n = (4 * k) + 3 & n is prime ) ) ) implies s1 = s2 )
assume that
A4: for n being Nat holds
( n in s1 iff ex k being Nat st
( n = (4 * k) + 3 & n is prime ) ) and
A5: for n being Nat holds
( n in s2 iff ex k being Nat st
( n = (4 * k) + 3 & n is prime ) ) ; :: thesis: s1 = s2
A6: for n being Element of NAT holds
( n in s1 iff S₁[n] )

proof

let n be Element of NAT ; :: thesis: ( n in s1 iff S₁[n] )
thus ( n in s1 implies S₁[n] ) :: thesis: ( S₁[n] implies n in s1 )

proof

assume n in s1 ; :: thesis: S₁[n]
then consider k being Nat such that
A7: ( n = (4 * k) + 3 & n is prime ) by A4;
thus S₁[n] by A7; :: thesis: verum

end;

assume S₁[n] ; :: thesis: n in s1
then consider k being Nat such that
A8: ( n = (4 * k) + 3 & (4 * k) + 3 is prime ) ;
thus n in s1 by A8, A4; :: thesis: verum

end;

A9: for n being Element of NAT holds
( n in s2 iff S₁[n] )

proof

let n be Element of NAT ; :: thesis: ( n in s2 iff S₁[n] )
thus ( n in s2 implies S₁[n] ) :: thesis: ( S₁[n] implies n in s2 )

proof

assume n in s2 ; :: thesis: S₁[n]
then consider k being Nat such that
A10: ( n = (4 * k) + 3 & n is prime ) by A5;
thus S₁[n] by A10; :: thesis: verum

end;

assume S₁[n] ; :: thesis: n in s2
then ex k being Nat st
( n = (4 * k) + 3 & (4 * k) + 3 is prime ) ;
hence n in s2 by A5; :: thesis: verum

end;

thus s1 = s2 from SUBSET_1:sch 2(A6, A9); :: thesis: verum