for x, X being set st x in MeetSections (J,F) & X in MeetSections (J,F) holds
x /\ X in MeetSections (J,F)
proof
let x, X be set ; :: thesis: ( x in MeetSections (J,F) & X in MeetSections (J,F) implies x /\ X in MeetSections (J,F) )
assume that
A1: x in MeetSections (J,F) and
A2: X in MeetSections (J,F) ; :: thesis: x /\ X in MeetSections (J,F)
consider E being non empty finite Subset of I, f being SigmaSection of E,F such that
A3: E c= J and
A4: x = meet (rng f) by A1, Def9;
defpred S1[ object ] means I in E;
deffunc H1( object ) -> set = f . I;
consider E9 being non empty finite Subset of I, f9 being SigmaSection of E9,F such that
A5: E9 c= J and
A6: X = meet (rng f9) by A2, Def9;
deffunc H2( object ) -> set = f9 . I;
defpred S2[ object ] means I in (E \ E9) \/ (E9 \ E);
deffunc H3( object ) -> set = (f . I) /\ (f9 . I);
consider h being Function such that
A7: ( dom h = E \/ E9 & ( for i being object st i in E \/ E9 holds
( ( S1[i] implies h . i = H1(i) ) & ( not S1[i] implies h . i = H2(i) ) ) ) ) from PARTFUN1:sch 1();
 deffunc H4( object ) -> set = h . I;
consider g being Function such that
A8: ( dom g = E \/ E9 & ( for i being object st i in E \/ E9 holds
( ( S2[i] implies g . i = H4(i) ) & ( not S2[i] implies g . i = H3(i) ) ) ) ) from PARTFUN1:sch 1();
 A9: for i being set st i in E \/ E9 holds
g . i in F . i
proof
let i be set ; :: thesis: ( i in E \/ E9 implies g . i in F . i )
assume A10: i in E \/ E9 ; :: thesis: g . i in F . i
per cases ( i in (E \ E9) \/ (E9 \ E) or not i in (E \ E9) \/ (E9 \ E) ) ;
suppose A11: i in (E \ E9) \/ (E9 \ E) ; :: thesis: g . i in F . i
h . i in F . i
proof
per cases ( i in E or not i in E ) ;
suppose A12: i in E ; :: thesis: h . i in F . i
then h . i = f . i by A7, A10;
hence h . i in F . i by A12, Def4; :: thesis: verum
end;
suppose not i in E ; :: thesis: h . i in F . i
then ( i in E9 & h . i = f9 . i ) by A7, A10, XBOOLE_0:def 3;
hence h . i in F . i by Def4; :: thesis: verum
end;
end;
end;
hence g . i in F . i by A8, A10, A11; :: thesis: verum
end;
suppose A13: not i in (E \ E9) \/ (E9 \ E) ; :: thesis: g . i in F . i
reconsider Fi = F . i as SigmaField of Omega by A10, Def2;
not i in E \+\ E9 by A13;
then ( i in E iff i in E9 ) by XBOOLE_0:1;
then ( f . i in F . i & f9 . i in F . i ) by A10, Def4, XBOOLE_0:def 3;
then A14: (f . i) /\ (f9 . i) is Event of Fi by PROB_1:19;
g . i = (f . i) /\ (f9 . i) by A8, A10, A13;
hence g . i in F . i by A14; :: thesis: verum
end;
end;
end;
rng g c= Sigma
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in Sigma )
assume y in rng g ; :: thesis: y in Sigma
then consider i being object such that
A15: ( i in dom g & y = g . i ) by FUNCT_1:def 3;
( y in F . i & F . i in bool Sigma ) by A8, A9, A15, FUNCT_2:5;
hence y in Sigma ; :: thesis: verum
end;
then g is Function of (E \/ E9),Sigma by A8, FUNCT_2:2;
then reconsider g = g as SigmaSection of E \/ E9,F by A9, Def4;
A16: x /\ X = meet (rng g)
proof
A17: meet (rng (g | (E /\ E9))) = (meet (rng (f | (E /\ E9)))) /\ (meet (rng (f9 | (E /\ E9))))
proof
per cases ( E /\ E9 = {} or not E /\ E9 = {} ) ;
suppose A18: E /\ E9 = {} ; :: thesis: meet (rng (g | (E /\ E9))) = (meet (rng (f | (E /\ E9)))) /\ (meet (rng (f9 | (E /\ E9))))
then A19: ( meet (rng (f | (E /\ E9))) = meet (rng {}) & meet (rng (f9 | (E /\ E9))) = meet (rng {}) ) ;
meet (rng (g | (E /\ E9))) = meet (rng {}) by A18
.= {} by SETFAM_1:def 1 ;
hence meet (rng (g | (E /\ E9))) = (meet (rng (f | (E /\ E9)))) /\ (meet (rng (f9 | (E /\ E9)))) by A19, SETFAM_1:def 1; :: thesis: verum
end;
suppose not E /\ E9 = {} ; :: thesis: meet (rng (g | (E /\ E9))) = (meet (rng (f | (E /\ E9)))) /\ (meet (rng (f9 | (E /\ E9))))
then reconsider EnE9 = E /\ E9 as non empty set ;
reconsider EE9 = EnE9 as Element of Fin EnE9 by FINSUB_1:def 5;
for B being Element of Fin EnE9 holds meet (rng (g | B)) = (meet (rng (f | B))) /\ (meet (rng (f9 | B)))
proof
defpred S3[ set ] means meet (rng (g | I)) = (meet (rng (f | I))) /\ (meet (rng (f9 | I)));
let B be Element of Fin EnE9; :: thesis: meet (rng (g | B)) = (meet (rng (f | B))) /\ (meet (rng (f9 | B)))
A20: for B9 being Element of Fin EnE9
for b being Element of EnE9 st S3[B9] & not b in B9 holds
S3[B9 \/ {b}]
proof
let B9 be Element of Fin EnE9; :: thesis: for b being Element of EnE9 st S3[B9] & not b in B9 holds
S3[B9 \/ {b}]
let b be Element of EnE9; :: thesis: ( S3[B9] & not b in B9 implies S3[B9 \/ {b}] )
assume that
A21: meet (rng (g | B9)) = (meet (rng (f | B9))) /\ (meet (rng (f9 | B9))) and
not b in B9 ; :: thesis: S3[B9 \/ {b}]
A22: dom (f | {b}) = (dom f) /\ {b} by RELAT_1:61;
dom f = E by FUNCT_2:def 1;
then A23: E /\ E9 c= dom f by XBOOLE_1:17;
then b in dom f ;
then A24: rng (f | {b}) = {((f | {b}) . b)} by A22, FUNCT_1:4, ZFMISC_1:46;
b in (E \ (E \/ E9)) \/ ((E /\ E) /\ E9) by XBOOLE_0:def 3;
then b in E \ (E \+\ E9) by XBOOLE_1:102;
then A25: not b in E \+\ E9 by XBOOLE_0:def 5;
A26: b in {b} by TARSKI:def 1;
b in dom f by A23;
then b in dom (f | {b}) by A26, RELAT_1:57;
then A27: rng (f | {b}) = {(f . b)} by A24, FUNCT_1:47;
then A28: meet (rng (f | {b})) = f . b by SETFAM_1:10;
A29: E /\ E9 c= E by XBOOLE_1:17;
A30: dom (f9 | {b}) = (dom f9) /\ {b} by RELAT_1:61;
dom f9 = E9 by FUNCT_2:def 1;
then A31: E /\ E9 c= dom f9 by XBOOLE_1:17;
then b in dom f9 ;
then A32: rng (f9 | {b}) = {((f9 | {b}) . b)} by A30, FUNCT_1:4, ZFMISC_1:46;
b in dom f9 by A31;
then b in dom (f9 | {b}) by A26, RELAT_1:57;
then A33: rng (f9 | {b}) = {(f9 . b)} by A32, FUNCT_1:47;
then A34: meet (rng (f9 | {b})) = f9 . b by SETFAM_1:10;
A35: for g being Function
for B9, b being set holds meet (rng (g | (B9 \/ {b}))) = meet ((rng (g | B9)) \/ (rng (g | {b})))
proof
let g be Function; :: thesis: for B9, b being set holds meet (rng (g | (B9 \/ {b}))) = meet ((rng (g | B9)) \/ (rng (g | {b})))
let B9, b be set ; :: thesis: meet (rng (g | (B9 \/ {b}))) = meet ((rng (g | B9)) \/ (rng (g | {b})))
rng (g | (B9 \/ {b})) = rng ((g | B9) \/ (g | {b})) by RELAT_1:78;
hence meet (rng (g | (B9 \/ {b}))) = meet ((rng (g | B9)) \/ (rng (g | {b}))) by RELAT_1:12; :: thesis: verum
end;
E c= dom g by A8, XBOOLE_1:7;
then A36: E /\ E9 c= dom g by A29;
then b is Element of dom g ;
then (dom g) /\ {b} = {b} by ZFMISC_1:46;
then dom (g | {b}) = {b} by RELAT_1:61;
then A37: rng (g | {b}) = {((g | {b}) . b)} by FUNCT_1:4;
( b in {b} & b in dom g ) by A36, TARSKI:def 1;
then b in dom (g | {b}) by RELAT_1:57;
then A38: rng (g | {b}) = {(g . b)} by A37, FUNCT_1:47;
then A39: meet (rng (g | {b})) = g . b by SETFAM_1:10;
E c= E \/ E9 by XBOOLE_1:7;
then A40: E /\ E9 c= E \/ E9 by A29;
then b in E \/ E9 ;
then A41: g . b = (f . b) /\ (f9 . b) by A8, A25;
per cases ( B9 = {} or B9 <> {} ) ;
suppose A42: B9 <> {} ; :: thesis: S3[B9 \/ {b}]
set z = the Element of B9;
B9 c= E /\ E9 by FINSUB_1:def 5;
then A43: B9 c= E \/ E9 by A40;
the Element of B9 in B9 by A42;
then dom (g | B9) <> {} by A8, A43;
then rng (g | B9) <> {} by RELAT_1:42;
then meet ((rng (g | B9)) \/ (rng (g | {b}))) = (meet (rng (g | B9))) /\ (meet (rng (g | {b}))) by A37, SETFAM_1:9;
then A44: meet (rng (g | (B9 \/ {b}))) = ((meet (rng (f | B9))) /\ (meet (rng (f9 | B9)))) /\ (g . b) by A21, A35, A39
.= (meet (rng (f | B9))) /\ ((meet (rng (f9 | B9))) /\ ((f . b) /\ (f9 . b))) by A41, XBOOLE_1:16
.= (meet (rng (f | B9))) /\ ((f . b) /\ ((meet (rng (f9 | B9))) /\ (f9 . b))) by XBOOLE_1:16
.= ((meet (rng (f | B9))) /\ (f . b)) /\ ((meet (rng (f9 | B9))) /\ (f9 . b)) by XBOOLE_1:16 ;
( B9 c= E /\ E9 & E /\ E9 c= E9 ) by FINSUB_1:def 5, XBOOLE_1:17;
then B9 c= E9 ;
then A45: B9 c= dom f9 by FUNCT_2:def 1;
( B9 c= E /\ E9 & E /\ E9 c= E ) by FINSUB_1:def 5, XBOOLE_1:17;
then B9 c= E ;
then A46: B9 c= dom f by FUNCT_2:def 1;
meet (rng (f | (B9 \/ {b}))) = meet ((rng (f | B9)) \/ (rng (f | {b}))) by A35
.= (meet (rng (f | B9))) /\ (meet (rng (f | {b}))) by A24, A42, A46, SETFAM_1:9 ;
then A47: (meet (rng (f | B9))) /\ (f . b) = meet (rng (f | (B9 \/ {b}))) by A27, SETFAM_1:10;
meet (rng (f9 | (B9 \/ {b}))) = meet ((rng (f9 | B9)) \/ (rng (f9 | {b}))) by A35
.= (meet (rng (f9 | B9))) /\ (meet (rng (f9 | {b}))) by A32, A42, A45, SETFAM_1:9 ;
hence S3[B9 \/ {b}] by A33, A44, A47, SETFAM_1:10; :: thesis: verum
end;
end;
end;
A48: S3[ {}. EnE9] ;
for B1 being Element of Fin EnE9 holds S3[B1] from SETWISEO:sch 2(A48, A20);
 hence meet (rng (g | B)) = (meet (rng (f | B))) /\ (meet (rng (f9 | B))) ; :: thesis: verum
end;
then meet (rng (g | EE9)) = (meet (rng (f | EE9))) /\ (meet (rng (f9 | EE9))) ;
hence meet (rng (g | (E /\ E9))) = (meet (rng (f | (E /\ E9)))) /\ (meet (rng (f9 | (E /\ E9)))) ; :: thesis: verum
end;
end;
end;
A49: for E, E9 being set
for g being Function st dom g = E \/ E9 holds
rng g = ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))
proof
let E, E9 be set ; :: thesis: for g being Function st dom g = E \/ E9 holds
rng g = ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))
let g be Function; :: thesis: ( dom g = E \/ E9 implies rng g = ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) )
( rng (g | (E /\ E9)) c= rng g & rng (g | (E \ E9)) c= rng g ) by RELAT_1:70;
then A50: (rng (g | (E /\ E9))) \/ (rng (g | (E \ E9))) c= rng g by XBOOLE_1:8;
assume A51: dom g = E \/ E9 ; :: thesis: rng g = ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))
thus rng g c= ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) :: according to XBOOLE_0:def 10 :: thesis: ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) c= rng g
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) )
assume y in rng g ; :: thesis: y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))
then consider i being object such that
A52: i in dom g and
A53: y = g . i by FUNCT_1:def 3;
per cases ( i in (E \ E9) \/ (E9 \ E) or not i in (E \ E9) \/ (E9 \ E) ) ;
suppose A54: i in (E \ E9) \/ (E9 \ E) ; :: thesis: y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))
y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))
proof
per cases ( i in E or not i in E ) ;
suppose A55: i in E ; :: thesis: y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))
A56: E /\ E9 c= E by XBOOLE_1:17;
E /\ ((E \ E9) \/ (E9 \ E)) = (E /\ (E \ E9)) \/ (E /\ (E9 \ E)) by XBOOLE_1:23
.= (E \ E9) \/ (E /\ (E9 \ E)) by XBOOLE_1:28
.= (E \ E9) \/ ((E /\ E9) \ E) by XBOOLE_1:49
.= (E \ E9) \/ {} by A56, XBOOLE_1:37 ;
then i in E \ E9 by A54, A55, XBOOLE_0:def 4;
then i in (dom g) /\ (E \ E9) by A52, XBOOLE_0:def 4;
then A57: i in dom (g | (E \ E9)) by RELAT_1:61;
then (g | (E \ E9)) . i = y by A53, FUNCT_1:47;
then y in rng (g | (E \ E9)) by A57, FUNCT_1:def 3;
then y in (rng (g | (E /\ E9))) \/ (rng (g | (E \ E9))) by XBOOLE_0:def 3;
hence y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) by XBOOLE_0:def 3; :: thesis: verum
end;
suppose A58: not i in E ; :: thesis: y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))
((E \ E9) \/ (E9 \ E)) \ E = ((E \ E9) \ E) \/ ((E9 \ E) \ E) by XBOOLE_1:42
.= {} \/ ((E9 \ E) \ E) by XBOOLE_1:37
.= E9 \ (E \/ E) by XBOOLE_1:41 ;
then i in E9 \ (E \/ E) by A54, A58, XBOOLE_0:def 5;
then i in (dom g) /\ (E9 \ E) by A52, XBOOLE_0:def 4;
then A59: i in dom (g | (E9 \ E)) by RELAT_1:61;
then (g | (E9 \ E)) . i = y by A53, FUNCT_1:47;
then y in rng (g | (E9 \ E)) by A59, FUNCT_1:def 3;
then y in (rng (g | (E \ E9))) \/ (rng (g | (E9 \ E))) by XBOOLE_0:def 3;
then y in (rng (g | (E /\ E9))) \/ ((rng (g | (E \ E9))) \/ (rng (g | (E9 \ E)))) by XBOOLE_0:def 3;
hence y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) by XBOOLE_1:4; :: thesis: verum
end;
end;
end;
hence y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) ; :: thesis: verum
end;
suppose A60: not i in (E \ E9) \/ (E9 \ E) ; :: thesis: y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E)))
A61: (E \/ E9) \ (E \+\ E9) = ((E \/ E9) \ (E \/ E9)) \/ (((E \/ E9) /\ E) /\ E9) by XBOOLE_1:102
.= {} \/ (((E \/ E9) /\ E) /\ E9) by XBOOLE_1:37
.= (E \/ E9) /\ (E /\ E9) by XBOOLE_1:16 ;
i in (E \/ E9) \ (E \+\ E9) by A51, A52, A60, XBOOLE_0:def 5;
then A62: i in dom (g | (E /\ E9)) by A51, A61, RELAT_1:61;
then (g | (E /\ E9)) . i = y by A53, FUNCT_1:47;
then y in rng (g | (E /\ E9)) by A62, FUNCT_1:def 3;
then y in (rng (g | (E /\ E9))) \/ (rng (g | (E \ E9))) by XBOOLE_0:def 3;
hence y in ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
rng (g | (E9 \ E)) c= rng g by RELAT_1:70;
hence ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) c= rng g by A50, XBOOLE_1:8; :: thesis: verum
end;
then A63: rng g = ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9)))) \/ (rng (g | (E9 \ E))) by A8;
A64: dom (g | (E9 \ E)) = (dom g) /\ (E9 \ E) by RELAT_1:61
.= (E \/ E9) /\ (E9 \ E) by FUNCT_2:def 1
.= ((E \/ E9) /\ E9) \ E by XBOOLE_1:49
.= E9 \ E by XBOOLE_1:21 ;
A65: for i being object st i in dom (g | (E9 \ E)) holds
(g | (E9 \ E)) . i = f9 . i
proof
let i be object ; :: thesis: ( i in dom (g | (E9 \ E)) implies (g | (E9 \ E)) . i = f9 . i )
assume A66: i in dom (g | (E9 \ E)) ; :: thesis: (g | (E9 \ E)) . i = f9 . i
then A67: i in (E \ E9) \/ (E9 \ E) by A64, XBOOLE_0:def 3;
not i in E by A64, A66, XBOOLE_0:def 5;
then f9 . i = h . i by A7, A66
.= g . i by A8, A66, A67 ;
hence (g | (E9 \ E)) . i = f9 . i by A66, FUNCT_1:47; :: thesis: verum
end;
dom (g | (E9 \ E)) = (E9 /\ E9) \ E by A64
.= E9 /\ (E9 \ E) by XBOOLE_1:49
.= (dom f9) /\ (E9 \ E) by FUNCT_2:def 1 ;
then A68: meet (rng (g | (E9 \ E))) = meet (rng (f9 | (E9 \ E))) by A65, FUNCT_1:46;
A69: dom (g | (E \ E9)) = (dom g) /\ (E \ E9) by RELAT_1:61
.= (E \/ E9) /\ (E \ E9) by FUNCT_2:def 1
.= ((E \/ E9) /\ E) \ E9 by XBOOLE_1:49
.= E \ E9 by XBOOLE_1:21 ;
A70: for i being object st i in dom (g | (E \ E9)) holds
(g | (E \ E9)) . i = f . i
proof
let i be object ; :: thesis: ( i in dom (g | (E \ E9)) implies (g | (E \ E9)) . i = f . i )
A71: E \ E9 c= E by XBOOLE_1:36;
assume A72: i in dom (g | (E \ E9)) ; :: thesis: (g | (E \ E9)) . i = f . i
then i in (E \ E9) \/ (E9 \ E) by A69, XBOOLE_0:def 3;
then g . i = h . i by A8, A72
.= f . i by A7, A69, A72, A71 ;
hence (g | (E \ E9)) . i = f . i by A72, FUNCT_1:47; :: thesis: verum
end;
dom (g | (E \ E9)) = (E /\ E) \ E9 by A69
.= E /\ (E \ E9) by XBOOLE_1:49
.= (dom f) /\ (E \ E9) by FUNCT_2:def 1 ;
then A73: meet (rng (g | (E \ E9))) = meet (rng (f | (E \ E9))) by A70, FUNCT_1:46;
per cases ( E /\ E9 = {} or not E /\ E9 = {} ) ;
suppose A81: not E /\ E9 = {} ; :: thesis: x /\ X = meet (rng g)
meet (rng g) = (meet (rng f)) /\ (meet (rng f9))
proof
per cases ( E \ E9 = {} or not E \ E9 = {} ) ;
suppose A82: E \ E9 = {} ; :: thesis: meet (rng g) = (meet (rng f)) /\ (meet (rng f9))
then A83: rng (g | (E \ E9)) = {} ;
A84: E c= E9 by A82, XBOOLE_1:37;
A85: E /\ E9 c= dom g by A8, XBOOLE_1:29;
meet (rng g) = (meet (rng f)) /\ (meet (rng f9))
proof
per cases ( E9 \ E = {} or E9 \ E <> {} ) ;
suppose E9 \ E = {} ; :: thesis: meet (rng g) = (meet (rng f)) /\ (meet (rng f9))
then E9 c= E by XBOOLE_1:37;
then A86: E = E9 by A84;
thus meet (rng g) = (meet (rng f)) /\ (meet (rng f9)) by A17, A86; :: thesis: verum
end;
suppose A87: E9 \ E <> {} ; :: thesis: meet (rng g) = (meet (rng f)) /\ (meet (rng f9))
( E9 \ E c= E9 & E9 c= E9 \/ E ) by XBOOLE_1:7, XBOOLE_1:36;
then E9 \ E c= dom g by A8;
then meet (rng g) = (meet (rng (g | (E /\ E9)))) /\ (meet (rng (g | (E9 \ E)))) by A63, A81, A83, A85, A87, SETFAM_1:9;
then A88: meet (rng g) = ((meet (rng f)) /\ (meet (rng (f9 | (E /\ E9))))) /\ (meet (rng (f9 | (E9 \ E)))) by A17, A68, A84, RELSET_1:19, XBOOLE_1:19;
A89: rng (f9 | (E \ E9)) = {} by A82;
E9 \ E c= E9 by XBOOLE_1:36;
then A90: E9 \ E c= dom f9 by FUNCT_2:def 1;
E /\ E9 c= E9 by XBOOLE_1:17;
then A91: E /\ E9 c= dom f9 by FUNCT_2:def 1;
( E9 \/ E = E9 & dom f9 = E9 ) by A84, FUNCT_2:def 1, XBOOLE_1:12;
then rng f9 = ((rng (f9 | (E /\ E9))) \/ (rng (f9 | (E \ E9)))) \/ (rng (f9 | (E9 \ E))) by A49
.= (rng (f9 | (E /\ E9))) \/ (rng (f9 | (E9 \ E))) by A89 ;
then meet (rng f9) = (meet (rng (f9 | (E /\ E9)))) /\ (meet (rng (f9 | (E9 \ E)))) by A81, A87, A91, A90, SETFAM_1:9;
hence meet (rng g) = (meet (rng f)) /\ (meet (rng f9)) by A88, XBOOLE_1:16; :: thesis: verum
end;
end;
end;
hence meet (rng g) = (meet (rng f)) /\ (meet (rng f9)) ; :: thesis: verum
end;
suppose A92: not E \ E9 = {} ; :: thesis: meet (rng g) = (meet (rng f)) /\ (meet (rng f9))
meet (rng g) = (meet (rng f)) /\ (meet (rng f9))
proof
( E \ E9 c= E & E c= dom g ) by A8, XBOOLE_1:7, XBOOLE_1:36;
then A93: rng (g | (E \ E9)) <> {} by A92, Th1, XBOOLE_1:1;
A94: E /\ E9 c= E \/ E9 by XBOOLE_1:29;
per cases ( E9 \ E = {} or not E9 \ E = {} ) ;
suppose A95: E9 \ E = {} ; :: thesis: meet (rng g) = (meet (rng f)) /\ (meet (rng f9))
then A96: rng (f | (E9 \ E)) = {} ;
E9 c= E by A95, XBOOLE_1:37;
then E = E \/ E9 by XBOOLE_1:12;
then dom f = E \/ E9 by FUNCT_2:def 1;
then A97: rng f = ((rng (f | (E /\ E9))) \/ (rng (f | (E \ E9)))) \/ (rng (f | (E9 \ E))) by A49
.= (rng (f | (E /\ E9))) \/ (rng (f | (E \ E9))) by A96 ;
E \ E9 c= E by XBOOLE_1:36;
then A98: E \ E9 c= dom f by FUNCT_2:def 1;
E9 c= E by A95, XBOOLE_1:37;
then A99: f9 | (E /\ E9) = f9 by RELSET_1:19, XBOOLE_1:19;
dom f = E by FUNCT_2:def 1;
then A100: rng (f | (E /\ E9)) <> {} by A81, Th1, XBOOLE_1:17;
rng (g | (E9 \ E)) = {} by A95;
then meet (rng g) = (meet (rng (g | (E /\ E9)))) /\ (meet (rng (g | (E \ E9)))) by A8, A63, A81, A94, A93, SETFAM_1:9
.= ((meet (rng (f | (E /\ E9)))) /\ (meet (rng (f | (E \ E9))))) /\ (meet (rng (f9 | (E /\ E9)))) by A17, A73, XBOOLE_1:16 ;
hence meet (rng g) = (meet (rng f)) /\ (meet (rng f9)) by A92, A99, A97, A100, A98, SETFAM_1:9; :: thesis: verum
end;
suppose A101: not E9 \ E = {} ; :: thesis: meet (rng g) = (meet (rng f)) /\ (meet (rng f9))
( E9 \ E c= E9 & E9 c= E \/ E9 ) by XBOOLE_1:7, XBOOLE_1:36;
then E9 \ E c= dom g by A8;
then meet (rng g) = (meet ((rng (g | (E /\ E9))) \/ (rng (g | (E \ E9))))) /\ (meet (rng (g | (E9 \ E)))) by A8, A63, A81, A94, A101, SETFAM_1:9
.= ((meet (rng (g | (E /\ E9)))) /\ (meet (rng (g | (E \ E9))))) /\ (meet (rng (g | (E9 \ E)))) by A8, A81, A94, A93, SETFAM_1:9 ;
then A102: meet (rng g) = (((meet (rng (f | (E /\ E9)))) /\ (meet (rng (f | (E \ E9))))) /\ (meet (rng (f9 | (E /\ E9))))) /\ (meet (rng (f9 | (E9 \ E)))) by A17, A73, A68, XBOOLE_1:16;
E /\ E9 c= E by XBOOLE_1:17;
then A103: E /\ E9 c= dom f by FUNCT_2:def 1;
E \/ (E /\ E9) = E by XBOOLE_1:12, XBOOLE_1:17;
then dom f = E \/ (E /\ E9) by FUNCT_2:def 1;
then A104: rng f = ((rng (f | (E /\ (E /\ E9)))) \/ (rng (f | (E \ (E /\ E9))))) \/ (rng (f | ((E /\ E9) \ E))) by A49;
E /\ E9 c= E by XBOOLE_1:17;
then (E /\ E9) \ E = {} by XBOOLE_1:37;
then A105: rng (f | ((E /\ E9) \ E)) = {} ;
E9 \ E c= E9 by XBOOLE_1:36;
then A106: E9 \ E c= dom f9 by FUNCT_2:def 1;
E /\ E9 c= E9 by XBOOLE_1:17;
then A107: E /\ E9 c= dom f9 by FUNCT_2:def 1;
E /\ E9 c= E9 by XBOOLE_1:17;
then A108: ( E9 \ E = E9 \ (E /\ E9) & (E /\ E9) \ E9 = {} ) by XBOOLE_1:37, XBOOLE_1:47;
E9 \/ (E /\ E9) = E9 by XBOOLE_1:12, XBOOLE_1:17;
then A109: dom f9 = E9 \/ (E /\ E9) by FUNCT_2:def 1;
E9 /\ (E /\ E9) = (E9 /\ E9) /\ E by XBOOLE_1:16
.= E /\ E9 ;
then rng f9 = ((rng (f9 | (E /\ E9))) \/ (rng (f9 | (E9 \ E)))) \/ (rng (f9 | {})) by A49, A109, A108;
then A110: meet (rng f9) = (meet (rng (f9 | (E /\ E9)))) /\ (meet (rng (f9 | (E9 \ E)))) by A81, A101, A107, A106, SETFAM_1:9;
E \ E9 c= E by XBOOLE_1:36;
then A111: E \ E9 c= dom f by FUNCT_2:def 1;
E /\ (E /\ E9) = (E /\ E) /\ E9 by XBOOLE_1:16
.= E /\ E9 ;
then rng f = (rng (f | (E /\ E9))) \/ (rng (f | (E \ E9))) by A104, A105, XBOOLE_1:47;
then meet (rng f) = (meet (rng (f | (E /\ E9)))) /\ (meet (rng (f | (E \ E9)))) by A81, A92, A103, A111, SETFAM_1:9;
hence meet (rng g) = (meet (rng f)) /\ (meet (rng f9)) by A110, A102, XBOOLE_1:16; :: thesis: verum
end;
end;
end;
hence meet (rng g) = (meet (rng f)) /\ (meet (rng f9)) ; :: thesis: verum
end;
end;
end;
hence x /\ X = meet (rng g) by A4, A6; :: thesis: verum
end;
end;
end;
for y being object st y in (meet (rng f)) /\ (meet (rng f9)) holds
y in Omega
proof
let y be object ; :: thesis: ( y in (meet (rng f)) /\ (meet (rng f9)) implies y in Omega )
consider S being object such that
A112: S in rng f by XBOOLE_0:def 1;
consider S9 being object such that
A113: S9 in rng f9 by XBOOLE_0:def 1;
assume A114: y in (meet (rng f)) /\ (meet (rng f9)) ; :: thesis: y in Omega
reconsider S = S, S9 = S9 as set by TARSKI:1;
y in meet (rng f9) by XBOOLE_0:def 4, A114;
then A115: y in S9 by A113, SETFAM_1:def 1;
y in meet (rng f) by A114, XBOOLE_0:def 4;
then y in S by A112, SETFAM_1:def 1;
then A116: y in S /\ S9 by A115, XBOOLE_0:def 4;
S /\ S9 is Event of Sigma by A112, A113, PROB_1:19;
hence y in Omega by A116; :: thesis: verum
end;
then reconsider xX = x /\ X as Subset of Omega by A4, A6, TARSKI:def 3;
E \/ E9 c= J by A3, A5, XBOOLE_1:8;
then xX in MeetSections (J,F) by A16, Def9;
hence x /\ X in MeetSections (J,F) ; :: thesis: verum
end;
hence MeetSections (J,F) is intersection_stable by FINSUB_1:def 2; :: thesis: verum