theorem :: FINANCE3:24

for Omega being set st Omega = {1,2,3,4} holds
( Omega in Special_SigmaField1 & {} in Special_SigmaField1 & {1,2} in Special_SigmaField2 & {3,4} in Special_SigmaField2 & Omega in Special_SigmaField2 & {} in Special_SigmaField2 & Omega in Trivial-SigmaField {1,2,3,4} & {} in Trivial-SigmaField {1,2,3,4} & {1} in Trivial-SigmaField {1,2,3,4} & {2} in Trivial-SigmaField {1,2,3,4} & {3} in Trivial-SigmaField {1,2,3,4} & {4} in Trivial-SigmaField {1,2,3,4} ) by EnLm1, EnLm2, EnLm3, PROB_1:5, EnLm4, PROB_1:4, ENUMSET1:def 2;