set A = { n where n is Nat : ( n + 1 is prime & n + 3 is prime & n + 7 is prime & n + 9 is prime & n + 13 is prime & n + 15 is prime ) } ;
A1: 5 = 4 + 1 ;
thus { n where n is Nat : ( n + 1 is prime & n + 3 is prime & n + 7 is prime & n + 9 is prime & n + 13 is prime & n + 15 is prime ) } c= {4} :: according to XBOOLE_0:def 10 :: thesis: {4} c= { n where n is Nat : ( n + 1 is prime & n + 3 is prime & n + 7 is prime & n + 9 is prime & n + 13 is prime & n + 15 is prime ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { n where n is Nat : ( n + 1 is prime & n + 3 is prime & n + 7 is prime & n + 9 is prime & n + 13 is prime & n + 15 is prime ) } or x in {4} )
assume x in { n where n is Nat : ( n + 1 is prime & n + 3 is prime & n + 7 is prime & n + 9 is prime & n + 13 is prime & n + 15 is prime ) } ; :: thesis: x in {4}
then consider n being Nat such that
A2: x = n and
A3: n + 1 is prime and
A4: n + 3 is prime and
A5: n + 7 is prime and
A6: n + 9 is prime and
A7: n + 13 is prime and
A8: n + 15 is prime ;

now :: thesis: not n <> 4

assume n <> 4 ; :: thesis: contradiction

per cases then ( n < 3 + 1 or n > 4 ) by XXREAL_0:1;

suppose n < 3 + 1 ; :: thesis: contradiction

then n <= 3 by NAT_1:13;
then not not n = 0 & ... & not n = 3 ;

per cases then ( n = 0 or n = 1 or n = 2 or n = 3 ) ;

suppose n = 0 ; :: thesis: contradiction

hence contradiction by A3; :: thesis: verum

end;

suppose n = 1 ; :: thesis: contradiction

hence contradiction by A4, INT_2:29; :: thesis: verum

end;

suppose n = 2 ; :: thesis: contradiction

hence contradiction by A5, NAT_4:57; :: thesis: verum

end;

suppose n = 3 ; :: thesis: contradiction

hence contradiction by A3, INT_2:29; :: thesis: verum

end;

end;

end;

suppose A9: n > 4 ; :: thesis: contradiction

( 5 divides n + 1 or 5 divides n + 7 or 5 divides n + 9 or 5 divides n + 13 or 5 divides n + 15 ) by Th62;
then ( 5 = n + 1 or 5 = n + 7 or 5 = n + 9 or 5 = n + 13 or 5 = n + 15 ) by A3, A5, A6, A7, A8;
hence contradiction by A1, A9, XREAL_1:8; :: thesis: verum

end;

end;

end;

hence x in {4} by A2, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {4} or x in { n where n is Nat : ( n + 1 is prime & n + 3 is prime & n + 7 is prime & n + 9 is prime & n + 13 is prime & n + 15 is prime ) } )
assume x in {4} ; :: thesis: x in { n where n is Nat : ( n + 1 is prime & n + 3 is prime & n + 7 is prime & n + 9 is prime & n + 13 is prime & n + 15 is prime ) }
then A10: x = 4 by TARSKI:def 1;
( 4 + 3 = 7 & 4 + 7 = 11 & 4 + 9 = 13 & 4 + 13 = 17 & 4 + 15 = 19 ) ;
hence x in { n where n is Nat : ( n + 1 is prime & n + 3 is prime & n + 7 is prime & n + 9 is prime & n + 13 is prime & n + 15 is prime ) } by A1, A10, PEPIN:59, PEPIN:60, NAT_4:26, NAT_4:27, NAT_4:28, NAT_4:29; :: thesis: verum