:: 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 = Special_SigmaField3 ) );