A1: ( (F _V) * (W1 .vertexSeq()) = (F .: W1) .vertexSeq() & (F _E) * (W1 .edgeSeq()) = (F .: W1) .edgeSeq() ) by Def37;
(F .: W1) .vertices() = rng ((F .: W1) .vertexSeq()) by GLIB_001:def 16;
hence (F .: W1) .vertices() c= rng (F _V) by A1, RELAT_1:26; :: according to GLIB_010:def 36 :: thesis: (F .: W1) .edges() c= rng (F _E)
(F .: W1) .edges() = rng ((F .: W1) .edgeSeq()) by GLIB_001:def 17;
hence (F .: W1) .edges() c= rng (F _E) by A1, RELAT_1:26; :: thesis: verum
thus verum ; :: thesis: verum