defpred S₁[ object ] means ex n being non zero Element of NAT st $1 = PFBrt (n,k);
A3: for A1, A2 being Subset of (SubstPoset (NAT,{k})) st ( for x being object holds
( x in A1 iff S₁[x] ) ) & ( for x being object holds
( x in A2 iff S₁[x] ) ) holds
A1 = A2 from HEYTING3:sch 1();
let A1, A2 be Subset of (SubstPoset (NAT,{k})); :: thesis: ( ( for x being object holds
( x in A1 iff ex n being non zero Element of NAT st x = PFBrt (n,k) ) ) & ( for x being object holds
( x in A2 iff ex n being non zero Element of NAT st x = PFBrt (n,k) ) ) implies A1 = A2 )
assume ( ( for x being object holds
( x in A1 iff S₁[x] ) ) & ( for x being object holds
( x in A2 iff S₁[x] ) ) ) ; :: thesis: A1 = A2
hence A1 = A2 by A3; :: thesis: verum