thus for D1, D2 being set st ( for x being object holds
( x in D1 iff S₃[x] ) ) & ( for x being object holds
( x in D2 iff S₃[x] ) ) holds
D1 = D2 from XBOOLE_0:sch 3(); :: thesis: verum