let E be non empty finite set ; :: thesis: for ASeq being SetSequence of E st ASeq is non-ascending holds
ex N being Element of NAT st
for m being Element of NAT st N <= m holds
Intersection ASeq = ASeq . m
let ASeq be SetSequence of E; :: thesis: ( ASeq is non-ascending implies ex N being Element of NAT st
for m being Element of NAT st N <= m holds
Intersection ASeq = ASeq . m )
assume A1: ASeq is non-ascending ; :: thesis: ex N being Element of NAT st
for m being Element of NAT st N <= m holds
Intersection ASeq = ASeq . m
then consider N0 being Element of NAT such that
A2: for m being Element of NAT st N0 <= m holds
ASeq . N0 = ASeq . m by Th14;
take N0 ; :: thesis: for m being Element of NAT st N0 <= m holds
Intersection ASeq = ASeq . m
let N be Element of NAT ; :: thesis: ( N0 <= N implies Intersection ASeq = ASeq . N )
assume N0 <= N ; :: thesis: Intersection ASeq = ASeq . N
then A3: ASeq . N = ASeq . N0 by A2;
thus Intersection ASeq = ASeq . N :: thesis: verum

proof

for x being set st x in Intersection ASeq holds
x in ASeq . N by PROB_1:13;
hence Intersection ASeq c= ASeq . N by TARSKI:def 3; :: according to XBOOLE_0:def 10 :: thesis: ASeq . N c= Intersection ASeq
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ASeq . N or x in Intersection ASeq )
assume A4: x in ASeq . N ; :: thesis: x in Intersection ASeq

now

let n be Element of NAT ; :: thesis: x in ASeq . b₁

per cases ( n <= N0 or N0 < n ) ;

suppose n <= N0 ; :: thesis: x in ASeq . b₁

then ASeq . N0 c= ASeq . n by A1, PROB_1:def 4;
hence x in ASeq . n by A3, A4; :: thesis: verum

end;

suppose N0 < n ; :: thesis: x in ASeq . b₁

hence x in ASeq . n by A2, A3, A4; :: thesis: verum

end;

end;

end;

hence x in Intersection ASeq by PROB_1:13; :: thesis: verum

end;