defpred S₁[ object ] means ex f being Function ex n being Element of omega st
( $1 in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) );
let U1, U2 be set ; :: thesis: ( ( for x being object holds
( x in U1 iff ex f being Function ex n being Element of omega st
( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) ) ) & ( for x being object holds
( x in U2 iff ex f being Function ex n being Element of omega st
( x in f . n & dom f = omega & f . 0 = X & ( for k being Nat holds f . (succ k) = union (f . k) ) ) ) ) implies U1 = U2 )
assume that
A13: for x being object holds
( x in U1 iff S₁[x] ) and
A14: for x being object holds
( x in U2 iff S₁[x] ) ; :: thesis: U1 = U2
thus U1 = U2 from XBOOLE_0:sch 2(A13, A14); :: thesis: verum