let Omega be set ; :: thesis: for Sigma being SigmaField of Omega

for ASeq, BSeq being SetSequence of Sigma

for B being Event of Sigma st ASeq is non-ascending & ( for n being Nat holds BSeq . n = (ASeq . n) /\ B ) holds

BSeq is non-ascending

let Sigma be SigmaField of Omega; :: thesis: for ASeq, BSeq being SetSequence of Sigma

for B being Event of Sigma st ASeq is non-ascending & ( for n being Nat holds BSeq . n = (ASeq . n) /\ B ) holds

BSeq is non-ascending

let ASeq, BSeq be SetSequence of Sigma; :: thesis: for B being Event of Sigma st ASeq is non-ascending & ( for n being Nat holds BSeq . n = (ASeq . n) /\ B ) holds

BSeq is non-ascending

let B be Event of Sigma; :: thesis: ( ASeq is non-ascending & ( for n being Nat holds BSeq . n = (ASeq . n) /\ B ) implies BSeq is non-ascending )

assume that

A1: ASeq is non-ascending and

A2: for n being Nat holds BSeq . n = (ASeq . n) /\ B ; :: thesis: BSeq is non-ascending

thus BSeq is non-ascending :: thesis: verum

for ASeq, BSeq being SetSequence of Sigma

for B being Event of Sigma st ASeq is non-ascending & ( for n being Nat holds BSeq . n = (ASeq . n) /\ B ) holds

BSeq is non-ascending

let Sigma be SigmaField of Omega; :: thesis: for ASeq, BSeq being SetSequence of Sigma

for B being Event of Sigma st ASeq is non-ascending & ( for n being Nat holds BSeq . n = (ASeq . n) /\ B ) holds

BSeq is non-ascending

let ASeq, BSeq be SetSequence of Sigma; :: thesis: for B being Event of Sigma st ASeq is non-ascending & ( for n being Nat holds BSeq . n = (ASeq . n) /\ B ) holds

BSeq is non-ascending

let B be Event of Sigma; :: thesis: ( ASeq is non-ascending & ( for n being Nat holds BSeq . n = (ASeq . n) /\ B ) implies BSeq is non-ascending )

assume that

A1: ASeq is non-ascending and

A2: for n being Nat holds BSeq . n = (ASeq . n) /\ B ; :: thesis: BSeq is non-ascending

thus BSeq is non-ascending :: thesis: verum

proof

let m be Nat; :: according to PROB_1:def 4 :: thesis: for b_{1} being set holds

( not m <= b_{1} or BSeq . b_{1} c= BSeq . m )

let n be Nat; :: thesis: ( not m <= n or BSeq . n c= BSeq . m )

assume m <= n ; :: thesis: BSeq . n c= BSeq . m

then ASeq . n c= ASeq . m by A1;

then (ASeq . n) /\ B c= (ASeq . m) /\ B by XBOOLE_1:26;

then BSeq . n c= (ASeq . m) /\ B by A2;

hence BSeq . n c= BSeq . m by A2; :: thesis: verum

end;( not m <= b

let n be Nat; :: thesis: ( not m <= n or BSeq . n c= BSeq . m )

assume m <= n ; :: thesis: BSeq . n c= BSeq . m

then ASeq . n c= ASeq . m by A1;

then (ASeq . n) /\ B c= (ASeq . m) /\ B by XBOOLE_1:26;

then BSeq . n c= (ASeq . m) /\ B by A2;

hence BSeq . n c= BSeq . m by A2; :: thesis: verum