let E be non empty finite set ; :: thesis: for ASeq being SetSequence of E st ASeq is non-ascending holds
ex N being Nat st
for m being Nat st N <= m holds
Intersection ASeq = ASeq . m
let ASeq be SetSequence of E; :: thesis: ( ASeq is non-ascending implies ex N being Nat st
for m being Nat st N <= m holds
Intersection ASeq = ASeq . m )
assume A1: ASeq is non-ascending ; :: thesis: ex N being Nat st
for m being Nat st N <= m holds
Intersection ASeq = ASeq . m
then consider N0 being Nat such that
A2: for m being Nat st N0 <= m holds
ASeq . N0 = ASeq . m by Th14;
take N0 ; :: thesis: for m being Nat st N0 <= m holds
Intersection ASeq = ASeq . m
let N be 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 object st x in Intersection ASeq holds
x in ASeq . N by PROB_1:13;
hence Intersection ASeq c= ASeq . N ; :: according to XBOOLE_0:def 10 :: thesis: ASeq . N c= Intersection ASeq
let x be object ; :: 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 :: thesis: for n being Nat holds x in ASeq . n
let n be Nat; :: thesis: x in ASeq . b1
per cases ( n <= N0 or N0 < n ) ;
suppose n <= N0 ; :: thesis: x in ASeq . b1
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 . b1
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;