let S be vertex-disjoint GraphUnionSet; :: thesis:
let G be GraphUnion of S; :: thesis:
set M = { (H .componentSet()) where H is Element of S : verum } ;

thus { (H .componentSet()) where H is Element of S : verum } is mutually-disjoint by Th66; :: thesis:
thus card S c= card { (H .componentSet()) where H is Element of S : verum } by Lm2; :: thesis:
let Y be set ; :: thesis:
assume Y in { (H .componentSet()) where H is Element of S : verum } ; :: thesis:
then consider H being Element of S such that
A1: Y = H .componentSet() ;
thus 1 c= card Y by A1, Lm3; :: thesis:

end;