thus ( IT is root implies dom IT = elementary_tree 0 ) :: thesis: ( dom IT = elementary_tree 0 implies IT is root )

proof

not dom IT is empty ;
then A1: not IT is empty ;
assume IT is root ; :: thesis: dom IT = elementary_tree 0
then consider x being set such that
A2: IT = {x} by A1, REALSET1:def 4;
x in IT by A2, TARSKI:def 1;
then consider x1, x2 being set such that
A3: x = [x1,x2] by RELAT_1:def 1;
( {} in dom IT & dom IT = {x1} ) by A2, A3, RELAT_1:23, TREES_1:47;
hence dom IT = elementary_tree 0 by TARSKI:def 1, TREES_1:56; :: thesis: verum

end;

thus ( dom IT = elementary_tree 0 implies IT is root ) by TREES_1:56; :: thesis: verum