:: deftheorem Def5 defines MP-WFF MODAL_1:def 5 :
for b₁ being DTree-set of [:NAT,NAT:] holds
( b₁ = MP-WFF iff ( ( for x being DecoratedTree of [:NAT,NAT:] st x in b₁ holds
x is finite ) & ( for x being finite DecoratedTree of [:NAT,NAT:] holds
( x in b₁ iff for v being Element of dom x holds
( branchdeg v <= 2 & ( not branchdeg v = 0 or x . v = [0,0] or ex k being Nat st x . v = [3,k] ) & ( not branchdeg v = 1 or x . v = [1,0] or x . v = [1,1] ) & ( branchdeg v = 2 implies x . v = [2,0] ) ) ) ) ) );