let A, B be non empty reflexive AltGraph ; :: thesis: for F being BimapStr over 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 over 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) ;
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:87;
[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:65;
consider p, p9 being object 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; :: thesis: verum