let V be non empty set ; :: thesis: for E being set
for S, T being Function of E,V st ex v being Element of V st
( S " {v} is infinite or T " {v} is infinite ) holds
not createGraph (V,E,S,T) is locally-finite
let E be set ; :: thesis: for S, T being Function of E,V st ex v being Element of V st
( S " {v} is infinite or T " {v} is infinite ) holds
not createGraph (V,E,S,T) is locally-finite
let S, T be Function of E,V; :: thesis: ( ex v being Element of V st
( S " {v} is infinite or T " {v} is infinite ) implies not createGraph (V,E,S,T) is locally-finite )
given v being Element of V such that A1: ( S " {v} is infinite or T " {v} is infinite ) ; :: thesis: not createGraph (V,E,S,T) is locally-finite
set G = createGraph (V,E,S,T);
reconsider v = v as Vertex of (createGraph (V,E,S,T)) ;

per cases ( S " {v} is infinite or T " {v} is infinite ) by A1;

suppose S " {v} is infinite ; :: thesis: not createGraph (V,E,S,T) is locally-finite

then (the_Source_of (createGraph (V,E,S,T))) " {v} is infinite ;
then v .edgesOut() is infinite by GLIB_000:147;
hence not createGraph (V,E,S,T) is locally-finite by Th25; :: thesis: verum

end;

suppose T " {v} is infinite ; :: thesis: not createGraph (V,E,S,T) is locally-finite

then (the_Target_of (createGraph (V,E,S,T))) " {v} is infinite ;
then v .edgesIn() is infinite by GLIB_000:147;
hence not createGraph (V,E,S,T) is locally-finite by Th25; :: thesis: verum

end;

end;