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 object such that
A2: IT = {x} by A1, ZFMISC_1:131;
x in IT by A2, TARSKI:def 1;
then consider x1, x2 being object such that
A3: x = [x1,x2] by RELAT_1:def 1;
( {} in dom IT & dom IT = {x1} ) by A2, A3, RELAT_1:9, TREES_1:22;
hence dom IT = elementary_tree 0 by TARSKI:def 1, TREES_1:29; :: thesis: verum

end;

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