take Free (S,X) ; :: thesis: ( Free (S,X) is X,S -terms & Free (S,X) is non-empty )
thus ( Free (S,X) is X,S -terms & Free (S,X) is non-empty ) ; :: thesis: verum