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 that
A1: G . 0 = {} and
A2: 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))
A3: for n being Element of NAT holds F . n c= F . 0

proof

defpred S₁[ Element of NAT ] means F . $1 c= F . 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 A2;
hence S₁[k + 1] by A5, XBOOLE_1:1; :: thesis: verum

end;

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

end;

A7: meet (rng F) c= F . 0

proof

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

end;

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