let X be set ; :: thesis: for B being SetSequence of X st B is non-ascending holds
superior_setsequence B = B
let B be SetSequence of X; :: thesis: ( B is non-ascending implies superior_setsequence B = B )
assume B is non-ascending ; :: thesis: superior_setsequence B = B
then for n being Nat holds (superior_setsequence B) . n = B . n by Th48;
then for n being Element of NAT holds (superior_setsequence B) . n = B . n ;
hence superior_setsequence B = B by FUNCT_2:63; :: thesis: verum