:: deftheorem Def9 defines Set2_of_SigmaField3 FINANCE3:def 12 :
for k being Element of {1,2,3} holds
( ( k <= 2 implies Set2_of_SigmaField3 k = Set1_of_SigmaField3 k ) & ( not k <= 2 implies Set2_of_SigmaField3 k = Trivial-SigmaField {1,2,3,4} ) );