for A, B being non empty AltGraph
for F being Contravariant FunctorStr over A,B st F is surjective holds
for a, b being Object of B st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being Object of A ex g being Morphism of c,d st
( b = F . c & a = F . d & <^c,d^> <> {} & f = F . g )