theorem Th34: :: GLIB_014:34

for S being Graph-membered set holds
( S is /\-tolerating iff ( S is \/-tolerating & meet (the_Vertices_of S) <> {} ) ) ;