let X be set ; :: thesis: for Y being non empty set
for x being set
for E being SetSequence of [:X,Y:]
for G being SetSequence of Y st E is non-ascending & ( for n being Nat holds G . n = X-section ((E . n),x) ) holds
G is non-ascending
let Y be non empty set ; :: thesis: for x being set
for E being SetSequence of [:X,Y:]
for G being SetSequence of Y st E is non-ascending & ( for n being Nat holds G . n = X-section ((E . n),x) ) holds
G is non-ascending
let x be set ; :: thesis: for E being SetSequence of [:X,Y:]
for G being SetSequence of Y st E is non-ascending & ( for n being Nat holds G . n = X-section ((E . n),x) ) holds
G is non-ascending
let E be SetSequence of [:X,Y:]; :: thesis: for G being SetSequence of Y st E is non-ascending & ( for n being Nat holds G . n = X-section ((E . n),x) ) holds
G is non-ascending
let G be SetSequence of Y; :: thesis: ( E is non-ascending & ( for n being Nat holds G . n = X-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 = X-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
X-section ((E . (n + 1)),x) c= X-section ((E . n),x) by Th14, A1, KURATO_0:def 3;
then G . (n + 1) c= X-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