theorem :: GLUNIR00:105

for V1 being non empty set
for V2 being non empty Subset of V1
for E1 being symmetric Relation of V1
for E2 being symmetric Relation of V2
for G1 being GraphFromSymRel of V1,E1
for G2 being GraphFromSymRel of V2,E2 st E2 c= E1 holds
ex F being PGraphMapping of G2,G1 st
( F is weak_SG-embedding & F _V = id V2 & ( for v, w being object holds
( not [v,w] in the_Edges_of G2 or (F _E) . [v,w] = [v,w] or (F _E) . [v,w] = [w,v] ) ) )