consider G being SimpleGraph such that
G is edgeless and
A: Vertices G = X by size0SG;
take G ; :: thesis: Vertices G = X
thus Vertices G = X by A; :: thesis: verum