let A, B be non empty reflexive AltGraph ; :: thesis: for F being BimapStr of A,B st F is coreflexive holds
for o being object of B ex o9 being object of A st F . o9 = o
let F be BimapStr of A,B; :: thesis: ( F is coreflexive implies for o being object of B ex o9 being object of A st F . o9 = o )
assume F is coreflexive ; :: thesis: for o being object of B ex o9 being object of A st F . o9 = o
then A1: id the carrier of B c= the ObjectMap of F .: (id the carrier of A) by Def10;
let o be object of B; :: thesis: ex o9 being object of A st F . o9 = o
reconsider oo = [o,o] as Element of [: the carrier of B, the carrier of B:] by ZFMISC_1:106;
[o,o] in id the carrier of B by RELAT_1:def 10;
then consider pp being Element of [: the carrier of A, the carrier of A:] such that
A2: pp in id the carrier of A and
A3: the ObjectMap of F . pp = oo by A1, FUNCT_2:116;
consider p, p9 being set such that
A4: pp = [p,p9] by RELAT_1:def 1;
A5: p = p9 by A2, A4, RELAT_1:def 10;
reconsider p = p as object of A by A2, A4, RELAT_1:def 10;
take p ; :: thesis: F . p = o
thus F . p = o by A3, A4, A5, MCART_1:7; :: thesis: verum