let X be set ; :: thesis: for S being SigmaField of X
for G, F being sequence of S st G . 0 = {} & ( for n being Nat holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds
union (rng G) = (F . 0) \ (meet (rng F))

let S be SigmaField of X; :: thesis: for G, F being sequence of S st G . 0 = {} & ( for n being Nat holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds
union (rng G) = (F . 0) \ (meet (rng F))

let G, F be sequence of S; :: thesis: ( G . 0 = {} & ( for n being Nat holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) implies union (rng G) = (F . 0) \ (meet (rng F)) )

assume that
A1: G . 0 = {} and
A2: for n being Nat holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ; :: thesis: union (rng G) = (F . 0) \ (meet (rng F))
A3: dom G = NAT by FUNCT_2:def 1;
thus union (rng G) c= (F . 0) \ (meet (rng F)) :: according to XBOOLE_0:def 10 :: thesis: (F . 0) \ (meet (rng F)) c= union (rng G)
proof
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in union (rng G) or A in (F . 0) \ (meet (rng F)) )
assume A in union (rng G) ; :: thesis: A in (F . 0) \ (meet (rng F))
then consider Z being set such that
A4: A in Z and
A5: Z in rng G by TARSKI:def 4;
consider n being object such that
A6: n in NAT and
A7: Z = G . n by ;
reconsider n = n as Element of NAT by A6;
consider k being Nat such that
A8: n = k + 1 by ;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
set Y = F . k;
A9: A in (F . 0) \ (F . k) by A2, A4, A7, A8;
then ( F . k in rng F & not A in F . k ) by ;
then A10: not A in meet (rng F) by SETFAM_1:def 1;
A in F . 0 by ;
hence A in (F . 0) \ (meet (rng F)) by ; :: thesis: verum
end;
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in (F . 0) \ (meet (rng F)) or A in union (rng G) )
assume A11: A in (F . 0) \ (meet (rng F)) ; :: thesis: A in union (rng G)
then not A in meet (rng F) by XBOOLE_0:def 5;
then A12: ex Y being set st
( Y in rng F & not A in Y ) by SETFAM_1:def 1;
A in F . 0 by ;
then consider Y being set such that
A13: A in F . 0 and
A14: Y in rng F and
A15: not A in Y by A12;
dom F = NAT by FUNCT_2:def 1;
then consider n being object such that
A16: n in NAT and
A17: Y = F . n by ;
reconsider n = n as Element of NAT by A16;
A in (F . 0) \ (F . n) by ;
then A18: A in G . (n + 1) by A2;
G . (n + 1) in rng G by FUNCT_2:4;
hence A in union (rng G) by ; :: thesis: verum