defpred S₁[ set ] means ex n being non empty Element of NAT st $1 = PFBrt n,k;
consider X being set such that
A1: for x being set holds
( x in X iff ( x in the carrier of (SubstPoset NAT ,{k}) & S₁[x] ) ) from XBOOLE_0:sch 1();
X c= the carrier of (SubstPoset NAT ,{k})

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in the carrier of (SubstPoset NAT ,{k}) )
assume x in X ; :: thesis: x in the carrier of (SubstPoset NAT ,{k})
hence x in the carrier of (SubstPoset NAT ,{k}) by A1; :: thesis: verum

end;

then reconsider X' = X as Subset of ;
take X' ; :: thesis: for x being set holds
( x in X' iff ex n being non empty Element of NAT st x = PFBrt n,k )
let x be set ; :: thesis: ( x in X' iff ex n being non empty Element of NAT st x = PFBrt n,k )
thus ( x in X' implies ex n being non empty Element of NAT st x = PFBrt n,k ) by A1; :: thesis: ( ex n being non empty Element of NAT st x = PFBrt n,k implies x in X' )
given n being non empty Element of NAT such that A2: x = PFBrt n,k ; :: thesis: x in X'
x is Element of by A2, Th28;
hence x in X' by A1, A2; :: thesis: verum