let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let F be SetSequence of S; :: thesis:
rng (superior_setsequence F) c= S by RELAT_1:def 19;
then reconsider G = superior_setsequence F as Function of NAT,S by FUNCT_2:6;
reconsider F1 = F, G1 = G as SetSequence of X ;
A1: for n being Element of NAT holds G . (n + 1) c= G . n

let n be Element of NAT ; :: thesis:
n <= n + 1 by NAT_1:12;
hence G . (n + 1) c= G . n by PROB_1:def 4; :: thesis:

end;

G . 0 = union { (F . k) where k is Element of NAT : 0 <= k } by SETLIM_1:def 3;
then A2: G . 0 = union (rng F) by SETLIM_1:5;
consider f being SetSequence of X such that
A3: lim_sup F1 = meet f and
A4: for n being Element of NAT holds f . n = Union (F1 ^\ n) by KURATO_0:def 2;

let n be Element of NAT ; :: thesis:
f . n = Union (F1 ^\ n) by A4;
hence f . n = G1 . n by Th2; :: thesis:

end;