scheme :: BINTREE2:sch 2
DecoratedBinTreeEx1{ F₁() -> non empty set , F₂() -> Element of F₁(), P₁[ object , object ], P₂[ object , object ] } :

ex D being binary DecoratedTree of F₁() st
( dom D = {0,1} * & D . {} = F₂() & ( for x being Node of D holds
( P₁[D . x,D . (x ^ <*0*>)] & P₂[D . x,D . (x ^ <*1*>)] ) ) )

provided

A1: for a being Element of F₁() ex b being Element of F₁() st P₁[a,b] and
A2: for a being Element of F₁() ex b being Element of F₁() st P₂[a,b]