let X be non empty set ; :: thesis: for Y, x being set
for E being SetSequence of [:X,Y:]
for G being SetSequence of X st E is non-ascending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) holds
G is non-ascending
let Y, x be set ; :: thesis: for E being SetSequence of [:X,Y:]
for G being SetSequence of X st E is non-ascending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) holds
G is non-ascending
let E be SetSequence of [:X,Y:]; :: thesis: for G being SetSequence of X st E is non-ascending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) holds
G is non-ascending
let G be SetSequence of X; :: thesis: ( E is non-ascending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) implies G is non-ascending )
assume that
A1: E is non-ascending and
A2: for n being Nat holds G . n = Y-section ((E . n),x) ; :: thesis: G is non-ascending
for n being Nat holds G . (n + 1) c= G . n

proof

let n be Nat; :: thesis: G . (n + 1) c= G . n
Y-section ((E . (n + 1)),x) c= Y-section ((E . n),x) by Th15, A1, KURATO_0:def 3;
then G . (n + 1) c= Y-section ((E . n),x) by A2;
hence G . (n + 1) c= G . n by A2; :: thesis: verum

end;

hence G is non-ascending by KURATO_0:def 3; :: thesis: verum