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 (superior_setsequence A3) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n)