defpred S₁[ object ] means ex n being non zero Element of NAT st $1 = PFBrt (n,k);
consider X being set such that
A1: for x being object 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})) by A1;
then reconsider X9 = X as Subset of (SubstPoset (NAT,{k})) ;
take X9 ; :: thesis: for x being object holds
( x in X9 iff ex n being non zero Element of NAT st x = PFBrt (n,k) )
let x be object ; :: thesis: ( x in X9 iff ex n being non zero Element of NAT st x = PFBrt (n,k) )
thus ( x in X9 implies ex n being non zero Element of NAT st x = PFBrt (n,k) ) by A1; :: thesis: ( ex n being non zero Element of NAT st x = PFBrt (n,k) implies x in X9 )
given n being non zero Element of NAT such that A2: x = PFBrt (n,k) ; :: thesis: x in X9
x is Element of (SubstPoset (NAT,{k})) by A2, Th25;
hence x in X9 by A1, A2; :: thesis: verum