scheme :: BINTREE2:sch 2
DecoratedBinTreeEx1{ F1() -> non empty set , F2() -> Element of F1(), P1[ object , object ], P2[ object , object ] } :
ex D being binary DecoratedTree of F1() st
( dom D = {0,1} * & D . {} = F2() & ( for x being Node of D holds
( P1[D . x,D . (x ^ <*0*>)] & P2[D . x,D . (x ^ <*1*>)] ) ) )
provided
A1: for a being Element of F1() ex b being Element of F1() st P1[a,b] and
A2: for a being Element of F1() ex b being Element of F1() st P2[a,b]