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