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