theorem :: FINANCE3:25

( Special_SigmaField1 c< Special_SigmaField2 & Special_SigmaField2 c< Trivial-SigmaField {1,2,3,4} ) by XX1, XX2;