let Omega, I be non empty set ; 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; 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; 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; MeetSections (J,F) is non empty Subset of Sigma
A1:
MeetSections (J,F) c= Sigma
MeetSections (J,F) is non empty set
hence
MeetSections (J,F) is non empty Subset of Sigma
by A1; verum