theorem :: GLIB_015:32

for S1, S2 being Graph-membered set st S1,S2 are_isomorphic holds
card S1 = card S2 by CARD_1:70;