let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is total & F is onto & F is semi-continuous & G2 is loopfull holds
G1 is loopfull
let F be PGraphMapping of G1,G2; :: thesis: ( F is total & F is onto & F is semi-continuous & G2 is loopfull implies G1 is loopfull )
assume A1: ( F is total & F is onto & F is semi-continuous ) ; :: thesis: ( not G2 is loopfull or G1 is loopfull )
G2 .loops() c= the_Edges_of G2 ;
then ( dom (F _V) = the_Vertices_of G1 & G2 .loops() c= rng (F _E) ) by A1, GLIB_010:def 11, GLIB_010:def 12;
hence ( not G2 is loopfull or G1 is loopfull ) by A1, Th8; :: thesis: verum