theorem :: SETLIM_1:34

for X being set
for A1, A2, A3 being SetSequence of X st ( for n being Nat holds A3 . n = (A1 . n) \/ (A2 . n) ) holds
for n being Nat holds ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n