set D = the set ;
take <*> the set ; :: thesis: <*> the set is empty
thus <*> the set is empty ; :: thesis: verum