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

meet (rng F) = (F . 0) \ (union (rng G))

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

meet (rng F) = (F . 0) \ (union (rng G))

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 meet (rng F) = (F . 0) \ (union (rng G)) )

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: meet (rng F) = (F . 0) \ (union (rng G))

A3: for n being Nat holds F . n c= F . 0

union (rng G) = (F . 0) \ (meet (rng F)) by A1, A2, Th4;

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

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

meet (rng F) = (F . 0) \ (union (rng G))

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

meet (rng F) = (F . 0) \ (union (rng G))

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 meet (rng F) = (F . 0) \ (union (rng G)) )

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: meet (rng F) = (F . 0) \ (union (rng G))

A3: for n being Nat holds F . n c= F . 0

proof

A7:
meet (rng F) c= F . 0
defpred S_{1}[ Nat] means F . $1 c= F . 0;

A4: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
;

thus for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A6, A4); :: thesis: verum

end;A4: for k being Nat st S

S

proof

A6:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A5: F . k c= F . 0 ; :: thesis: S_{1}[k + 1]

F . (k + 1) c= F . k by A2;

hence S_{1}[k + 1]
by A5, XBOOLE_1:1; :: thesis: verum

end;assume A5: F . k c= F . 0 ; :: thesis: S

F . (k + 1) c= F . k by A2;

hence S

thus for n being Nat holds S

proof

A9:
(F . 0) /\ (meet (rng F)) = (F . 0) \ ((F . 0) \ (meet (rng F)))
by XBOOLE_1:48;
set X = the Element of rng F;

let A be object ; :: 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 object st

( n in NAT & F . n = the Element of rng F ) by FUNCT_1:def 3;

then A8: the Element of rng F c= F . 0 by A3;

assume A in meet (rng F) ; :: thesis: A in F . 0

then A in the Element of rng F by SETFAM_1:def 1;

hence A in F . 0 by A8; :: thesis: verum

end;let A be object ; :: 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 object st

( n in NAT & F . n = the Element of rng F ) by FUNCT_1:def 3;

then A8: the Element of rng F c= F . 0 by A3;

assume A in meet (rng F) ; :: thesis: A in F . 0

then A in the Element of rng F by SETFAM_1:def 1;

hence A in F . 0 by A8; :: thesis: verum

union (rng G) = (F . 0) \ (meet (rng F)) by A1, A2, Th4;

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