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

proof

let x be object ; :: 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
A2: x = f and
A3: f is 1 -element ;
consider a being set such that
A4: a in union G and
A5: f = {a} by A3, Th9;
consider y being set such that
A6: a in y and
A7: y in G by A4, TARSKI:def 4;
{a} c= y by A6, ZFMISC_1:31;
hence x in G by A7, A5, A2, CLASSES1:def 1; :: thesis: verum

end;

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