{ q where q is Prime : ex p being Prime st
( p < q & q divides ((p -' 1) !) + 1 ) } c= { q where q is Prime : ex n being Nat st
( n < q & q divides ((n -' 1) !) + 1 ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Prime : ex p being Prime st
( p < q & q divides ((p -' 1) !) + 1 ) } or x in { q where q is Prime : ex n being Nat st
( n < q & q divides ((n -' 1) !) + 1 ) } )
assume x in { q where q is Prime : ex p being Prime st
( p < q & q divides ((p -' 1) !) + 1 ) } ; :: thesis: x in { q where q is Prime : ex n being Nat st
( n < q & q divides ((n -' 1) !) + 1 ) }
then ex q being Prime st
( q = x & ex p being Prime st
( p < q & q divides ((p -' 1) !) + 1 ) ) ;
hence x in { q where q is Prime : ex n being Nat st
( n < q & q divides ((n -' 1) !) + 1 ) } ; :: thesis: verum

end;

hence { q where q is Prime : ex n being Nat st
( n < q & q divides ((n -' 1) !) + 1 ) } is infinite by Th26; :: thesis: verum