defpred S1[ Element of [:NAT,NAT:]] means ex n1, n2 being Nat st
( n1 = $1 `1 & n2 = $1 `2 & n <= n1 & n <= n2 );
ex B being Subset of [:NAT,NAT:] st
for x being Element of [:NAT,NAT:] holds
( x in B iff S1[x] )
from SUBSET_1:sch 3();
hence
ex b1 being Subset of [:NAT,NAT:] st
for x being Element of [:NAT,NAT:] holds
( x in b1 iff ex n1, n2 being Nat st
( n1 = x `1 & n2 = x `2 & n <= n1 & n <= n2 ) )
; verum