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

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