consider s being Subset of NAT such that
A1: for x being set holds
( x in s iff ( x in NAT & S₁[x] ) ) from SUBSET_1:sch 1();
take s ; :: thesis: for n being Nat holds
( n in s iff ex k being Nat st
( n = (4 * k) + 3 & n is prime ) )
let n be Nat; :: thesis: ( n in s iff ex k being Nat st
( n = (4 * k) + 3 & n is prime ) )
thus ( n in s implies ex k being Nat st
( n = (4 * k) + 3 & n is prime ) ) :: thesis: ( ex k being Nat st
( n = (4 * k) + 3 & n is prime ) implies n in s )

proof

assume n in s ; :: thesis: ex k being Nat st
( n = (4 * k) + 3 & n is prime )
then consider k being Nat such that
A2: ( n = (4 * k) + 3 & (4 * k) + 3 is prime ) by A1;
thus ex k being Nat st
( n = (4 * k) + 3 & n is prime ) by A2; :: thesis: verum

end;

given k being Nat such that A3: ( n = (4 * k) + 3 & n is prime ) ; :: thesis: n in s
thus n in s by A3, A1; :: thesis: verum