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
proof
defpred S1[ Nat] means F . $1 c= F . 0;
A4: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: F . k c= F . 0 ; :: thesis: S1[k + 1]
F . (k + 1) c= F . k by A2;
hence S1[k + 1] by A5, XBOOLE_1:1; :: thesis: verum
end;
A6: S1[ 0 ] ;
thus for n being Nat holds S1[n] from NAT_1:sch 2(A6, A4); :: thesis: verum
end;
A7: meet (rng F) c= F . 0
proof
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;
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, Th4;
hence meet (rng F) = (F . 0) \ (union (rng G)) by A7, A9, XBOOLE_1:28; :: thesis: verum