defpred S1[ Element of [:NAT,NAT:]] means ex n1, n2 being Nat st
( n1 = $1 `1 & n2 = $1 `2 & n1 < n & n2 < n );
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 & n1 < n & n2 < n ) )
; verum