for X, x being set
for A1 being SetSequence of X holds
( x in Union A1 iff ex n being Nat st x in A1 . n )