take elementary_tree 0 ; :: thesis: ( elementary_tree 0 is binary & elementary_tree 0 is finite )
thus ( elementary_tree 0 is binary & elementary_tree 0 is finite ) ; :: thesis: verum