reconsider G = {{},{{}}} as SimpleGraph by Th25;
set A = union G;
union G = {{}} by Th8;
then not G is void ;
hence ex b₁ being SimpleGraph st
( b₁ is with_finite_stability# & not b₁ is void ) ; :: thesis: verum