take FinTrees ; :: thesis: ( FinTrees is constituted-FinTrees & not FinTrees is empty )
thus ( FinTrees is constituted-FinTrees & not FinTrees is empty ) ; :: thesis: verum