let n be Nat; :: thesis: for X being set
for A1, A2 being SetSequence of X holds ((superior_setsequence A1) . n) \ ((superior_setsequence A2) . n) c= (superior_setsequence (A1 (\) A2)) . n
let X be set ; :: thesis: for A1, A2 being SetSequence of X holds ((superior_setsequence A1) . n) \ ((superior_setsequence A2) . n) c= (superior_setsequence (A1 (\) A2)) . n
let A1, A2 be SetSequence of X; :: thesis: ((superior_setsequence A1) . n) \ ((superior_setsequence A2) . n) c= (superior_setsequence (A1 (\) A2)) . n
((superior_setsequence A1) . n) \ ((superior_setsequence A2) . n) = (Union (A1 ^\ n)) \ ((superior_setsequence A2) . n) by Th2
.= (Union (A1 ^\ n)) \ (Union (A2 ^\ n)) by Th2 ;
then ((superior_setsequence A1) . n) \ ((superior_setsequence A2) . n) c= Union ((A1 ^\ n) (\) (A2 ^\ n)) by Th10;
then ((superior_setsequence A1) . n) \ ((superior_setsequence A2) . n) c= Union ((A1 (\) A2) ^\ n) by Th6;
hence ((superior_setsequence A1) . n) \ ((superior_setsequence A2) . n) c= (superior_setsequence (A1 (\) A2)) . n by Th2; :: thesis: verum