take Free (S,X) ; :: thesis: ( Free (S,X) is all_vars_including & Free (S,X) is inheriting_operations & Free (S,X) is free_in_itself )
thus ( Free (S,X) is all_vars_including & Free (S,X) is inheriting_operations & Free (S,X) is free_in_itself ) ; :: thesis: verum