let S be Graph-membered set ; :: thesis: ( S is /\-tolerating implies ( S is \/-tolerating & not S is empty ) )
assume A1: S is /\-tolerating ; :: thesis: ( S is \/-tolerating & not S is empty )
hence S is \/-tolerating ; :: thesis: not S is empty
assume S is empty ; :: thesis: contradiction
then the_Vertices_of S = {} ;
hence contradiction by A1, SETFAM_1:def 1; :: thesis: verum