let Omega, I be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for F being ManySortedSigmaField of I,Sigma
for J being non empty Subset of I holds MeetSections (J,F) is non empty Subset of Sigma
let Sigma be SigmaField of Omega; :: thesis: for F being ManySortedSigmaField of I,Sigma
for J being non empty Subset of I holds MeetSections (J,F) is non empty Subset of Sigma
let F be ManySortedSigmaField of I,Sigma; :: thesis: for J being non empty Subset of I holds MeetSections (J,F) is non empty Subset of Sigma
let J be non empty Subset of I; :: thesis: MeetSections (J,F) is non empty Subset of Sigma
A1: MeetSections (J,F) c= Sigma

proof

let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in MeetSections (J,F) or X in Sigma )
assume X in MeetSections (J,F) ; :: thesis: X in Sigma
then consider E being non empty finite Subset of I, f being SigmaSection of E,F such that
E c= J and
A2: X = meet (rng f) by Def9;
reconsider Ee = E as Element of Fin E by FINSUB_1:def 5;
for B being Element of Fin E holds meet (rng (f | B)) in Sigma

proof

defpred S₁[ set ] means meet (rng (f | $1)) in Sigma;
let B be Element of Fin E; :: thesis: meet (rng (f | B)) in Sigma
A3: for B9 being Element of Fin E
for b being Element of E st S₁[B9] & not b in B9 holds
S₁[B9 \/ {b}]

proof

let B9 be Element of Fin E; :: thesis: for b being Element of E st S₁[B9] & not b in B9 holds
S₁[B9 \/ {b}]
let b be Element of E; :: thesis: ( S₁[B9] & not b in B9 implies S₁[B9 \/ {b}] )
assume that
A4: meet (rng (f | B9)) in Sigma and
not b in B9 ; :: thesis: S₁[B9 \/ {b}]
A5: rng (f | (B9 \/ {b})) = rng ((f | B9) \/ (f | {b})) by RELAT_1:78
.= (rng (f | B9)) \/ (rng (f | {b})) by RELAT_1:12 ;
( dom f = E & b in {b} ) by FUNCT_2:def 1, TARSKI:def 1;
then A6: f . b in rng (f | {b}) by FUNCT_1:50;
A7: b is Element of dom f by FUNCT_2:def 1;
then (dom f) /\ {b} = {b} by ZFMISC_1:46;
then dom (f | {b}) = {b} by RELAT_1:61;
then A8: rng (f | {b}) = {((f | {b}) . b)} by FUNCT_1:4;
b in {b} by TARSKI:def 1;
then b in dom (f | {b}) by A7, RELAT_1:57;
then rng (f | {b}) = {(f . b)} by A8, FUNCT_1:47;
then A9: meet (rng (f | {b})) is Event of Sigma by SETFAM_1:10;

per cases ( rng (f | B9) = {} or not rng (f | B9) = {} ) ;

suppose rng (f | B9) = {} ; :: thesis: S₁[B9 \/ {b}]

hence S₁[B9 \/ {b}] by A9, A5; :: thesis: verum

end;

suppose not rng (f | B9) = {} ; :: thesis: S₁[B9 \/ {b}]

then meet (rng (f | (B9 \/ {b}))) = (meet (rng (f | B9))) /\ (meet (rng (f | {b}))) by A5, A6, SETFAM_1:9;
then meet (rng (f | (B9 \/ {b}))) is Event of Sigma by A4, A9, PROB_1:19;
hence S₁[B9 \/ {b}] ; :: thesis: verum

end;

end;

end;

meet (rng (f | {})) = {} by SETFAM_1:def 1;
then A10: S₁[ {}. E] by PROB_1:4;
for B1 being Element of Fin E holds S₁[B1] from SETWISEO:sch 2(A10, A3);
hence meet (rng (f | B)) in Sigma ; :: thesis: verum

end;

then meet (rng (f | Ee)) in Sigma ;
hence X in Sigma by A2; :: thesis: verum

end;

MeetSections (J,F) is non empty set

proof

set E = the non empty finite Subset of J;
consider f being Function such that
A11: dom f = the non empty finite Subset of J and
A12: rng f = {{}} by FUNCT_1:5;
reconsider E = the non empty finite Subset of J as non empty finite Subset of I by XBOOLE_1:1;
A13: meet (rng f) = {} by A12, SETFAM_1:10;
rng f c= Sigma

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in Sigma )
assume y in rng f ; :: thesis: y in Sigma
then y = {} by A12, TARSKI:def 1;
hence y in Sigma by PROB_1:4; :: thesis: verum

end;

then reconsider f = f as Function of E,Sigma by A11, FUNCT_2:2;
for i being set st i in E holds
f . i in F . i

proof

let i be set ; :: thesis: ( i in E implies f . i in F . i )
assume A14: i in E ; :: thesis: f . i in F . i
then reconsider Fi = F . i as SigmaField of Omega by Def2;
f . i in rng f by A11, A14, FUNCT_1:def 3;
then f . i = {} by A12, TARSKI:def 1;
then f . i in Fi by PROB_1:4;
hence f . i in F . i ; :: thesis: verum

end;

then reconsider f = f as SigmaSection of E,F by Def4;
reconsider mrf = meet (rng f) as Subset of Omega by A13, XBOOLE_1:2;
mrf in MeetSections (J,F) by Def9;
hence MeetSections (J,F) is non empty set ; :: thesis: verum

end;

hence MeetSections (J,F) is non empty Subset of Sigma by A1; :: thesis: verum