theorem Th33: :: YELLOW20:33

for A, B being non empty AltGraph
for F being Covariant 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
( a = F . c & b = F . d & <^c,d^> <> {} & f = F . g )