let G be finite SimpleGraph; :: thesis: order G <= card G
set uG = union G;
A: card (singletons (union G)) = card (union G) by BSPACE:41;
singletons (union G) c= G

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in singletons (union G) or x in G )
assume x in singletons (union G) ; :: thesis: x in G
then consider f being Subset of (union G) such that
B: x = f and
C: f is 1 -element ;
consider a being set such that
D: a in union G and
E: f = {a} by C, BSPACEdef9;
consider y being set such that
F: a in y and
G: y in G by D, TARSKI:def 4;
{a} c= y by F, ZFMISC_1:31;
hence x in G by G, E, B, CLASSES1:def 1; :: thesis: verum

end;

hence order G <= card G by A, NAT_1:43; :: thesis: verum