let X be set ; :: thesis: for S being SigmaField of X
for G, F being Function of NAT ,S st G . 0 = {} & ( for n being Element of NAT holds
( G . (n + 1) = (F . 0 ) \ (F . n) & F . (n + 1) c= F . n ) ) holds
meet (rng F) = (F . 0 ) \ (union (rng G))
let S be SigmaField of X; :: thesis: for G, F being Function of NAT ,S st G . 0 = {} & ( for n being Element of NAT holds
( G . (n + 1) = (F . 0 ) \ (F . n) & F . (n + 1) c= F . n ) ) holds
meet (rng F) = (F . 0 ) \ (union (rng G))
let G, F be Function of NAT ,S; :: thesis: ( G . 0 = {} & ( for n being Element of NAT holds
( G . (n + 1) = (F . 0 ) \ (F . n) & F . (n + 1) c= F . n ) ) implies meet (rng F) = (F . 0 ) \ (union (rng G)) )
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: meet (rng F) = (F . 0 ) \ (union (rng G))
A2: for n being Element of NAT holds F . n c= F . 0

proof

defpred S₁[ Element of NAT ] means F . $1 c= F . 0 ;
A3: S₁[ 0 ] ;
A4: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: F . k c= F . 0 ; :: thesis: S₁[k + 1]
F . (k + 1) c= F . k by A1;
hence S₁[k + 1] by A5, XBOOLE_1:1; :: thesis: verum

end;

thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A4); :: thesis: verum

end;

A6: union (rng G) = (F . 0 ) \ (meet (rng F)) by A1, Th6;
A7: meet (rng F) c= F . 0

proof

let A be set ; :: according to TARSKI:def 3 :: thesis: ( not A in meet (rng F) or A in F . 0 )
assume A8: A in meet (rng F) ; :: thesis: A in F . 0
A9: dom F = NAT by FUNCT_2:def 1;
consider X being Element of rng F;
A10: A in X by A8, SETFAM_1:def 1;
ex n being set st
( n in NAT & F . n = X ) by A9, FUNCT_1:def 5;
then X c= F . 0 by A2;
hence A in F . 0 by A10; :: thesis: verum

end;

(F . 0 ) /\ (meet (rng F)) = (F . 0 ) \ ((F . 0 ) \ (meet (rng F))) by XBOOLE_1:48;
hence meet (rng F) = (F . 0 ) \ (union (rng G)) by A6, A7, XBOOLE_1:28; :: thesis: verum