let X be set ; :: thesis:
let S be SigmaField of X; :: thesis:
let G, F be Function of NAT ,S; :: thesis:
assume A1: ( G . 0 = {} & ( for n being Element of NAT holds
( G . (n + 1) = (F . 0 ) \ (F . n) & F . (n + 1) c= F . n ) ) ) ; :: thesis:
A2: ( dom F = NAT & dom G = NAT & rng F c= S & rng G c= S ) by FUNCT_2:def 1, RELAT_1:def 19;
thus union (rng G) c= (F . 0 ) \ (meet (rng F)) :: according to XBOOLE_0:def 10 :: thesis:

proof

let A be set ; :: according to TARSKI:def 3 :: thesis:
assume A in union (rng G) ; :: thesis:
then consider Z being set such that
A3: ( A in Z & Z in rng G ) by TARSKI:def 4;
consider n being set such that
A4: ( n in NAT & Z = G . n ) by A2, A3, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A4;
consider k being Nat such that
A5: n = k + 1 by A1, A3, A4, NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A6: A in (F . 0 ) \ (F . k) by A1, A3, A4, A5;
then A7: ( A in F . 0 & not A in F . k ) by XBOOLE_0:def 5;
set Y = F . k;
( rng F <> {} & F . k in rng F & not A in F . k ) by A6, FUNCT_2:6, XBOOLE_0:def 5;
then not A in meet (rng F) by SETFAM_1:def 1;
hence A in (F . 0 ) \ (meet (rng F)) by A7, XBOOLE_0:def 5; :: thesis:

end;

let A be set ; :: according to TARSKI:def 3 :: thesis:
assume A in (F . 0 ) \ (meet (rng F)) ; :: thesis:
then ( A in F . 0 & not A in meet (rng F) ) by XBOOLE_0:def 5;
then ( A in F . 0 & ex Y being set st
( Y in rng F & not A in Y ) ) by SETFAM_1:def 1;
then consider Y being set such that
A8: ( A in F . 0 & Y in rng F & not A in Y ) ;
consider n being set such that
A9: ( n in NAT & Y = F . n ) by A2, A8, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A9;
A in (F . 0 ) \ (F . n) by A8, A9, XBOOLE_0:def 5;
then A10: A in G . (n + 1) by A1;
G . (n + 1) in rng G by FUNCT_2:6;
hence A in union (rng G) by A10, TARSKI:def 4; :: thesis: