let G be SimpleGraph; :: thesis: for x being object holds
( x in Vertices G iff {x} in G )
let x be object ; :: thesis: ( x in Vertices G iff {x} in G )
thus ( x in Vertices G implies {x} in G ) :: thesis: ( {x} in G implies x in Vertices G )

proof

assume x in Vertices G ; :: thesis: {x} in G
then consider y being set such that
A1: x in y and
A2: y in G by TARSKI:def 4;
{x} c= y by A1, ZFMISC_1:31;
hence {x} in G by A2, CLASSES1:def 1; :: thesis: verum

end;

x in {x} by TARSKI:def 1;
hence ( {x} in G implies x in Vertices G ) by TARSKI:def 4; :: thesis: verum