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)) ;