let G be Cycle-like _Graph; :: thesis: G .order() = G .size()
2 * (G .size()) = 2 *` (G .size()) by FIELD_5:2
.= 2 *` (G .order()) by GLIB_016:58
.= 2 * (G .order()) by FIELD_5:2 ;
hence G .order() = G .size() ; :: thesis: verum