take set_of_constant_RV F ; :: thesis: ( set_of_constant_RV F is F -random-membered & not set_of_constant_RV F is empty )
thus ( set_of_constant_RV F is F -random-membered & not set_of_constant_RV F is empty ) ; :: thesis: verum