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
proof
let m be Nat; :: according to PROB_1:def 4 :: thesis: for b1 being set holds
( not m <= b1 or BSeq . b1 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;