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 Special_SigmaField3 & {} in Special_SigmaField3 & {1} in Special_SigmaField3 & {2} in Special_SigmaField3 & {3} in Special_SigmaField3 & {4} in Special_SigmaField3 ) by EnLm1, EnLm2, EnLm3, PROB_1:5, EnLm4, PROB_1:4, ENUMSET1:def 2;