t2:=th4"l.some"([x:sigma]nissetprop(s0,t0,x),m,s):not(nissetprop(s0,t0,s))
t3:=<s>l:not(nissetprop(t0,s0,s))
l@t4:=isseti(s0,t0,[x:sigma][y:esti(x,s0)]t1(s0,t0,x,t2(x),y),[x:sigma][y:esti(x,t0)]t1(t0,s0,x,t3(x),y)):is(set,s0,t0)
t2:=th4"l.some"([x:sigma]nissetprop(s0,t0,x),m,s):not(nissetprop(s0,t0,s))
t3:=<s>l:not(nissetprop(t0,s0,s))
l@t4:=isseti(s0,t0,[x:sigma][y:esti(x,s0)]t1(s0,t0,x,t2(x),y),[x:sigma][y:esti(x,t0)]t1(t0,s0,x,t3(x),y)):is(set,s0,t0)