let S1, S2 be non empty transitive strict SubCatStr of C; ( the carrier of S1 = the carrier of C & the Arrows of S1 cc= the Arrows of C & ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of S1 . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) ) ) & the carrier of S2 = the carrier of C & the Arrows of S2 cc= the Arrows of C & ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of S2 . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) ) ) implies S1 = S2 )
assume that
A76:
the carrier of S1 = the carrier of C
and
A77:
the Arrows of S1 cc= the Arrows of C
and
A78:
for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of S1 . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) )
and
A79:
the carrier of S2 = the carrier of C
and
A80:
the Arrows of S2 cc= the Arrows of C
and
A81:
for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of S2 . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) )
; S1 = S2
now for i being object st i in [: the carrier of C, the carrier of C:] holds
the Arrows of S1 . i = the Arrows of S2 . ilet i be
object ;
( i in [: the carrier of C, the carrier of C:] implies the Arrows of S1 . i = the Arrows of S2 . i )assume A82:
i in [: the carrier of C, the carrier of C:]
;
the Arrows of S1 . i = the Arrows of S2 . ithen consider o1,
o2 being
object such that A83:
(
o1 in the
carrier of
C &
o2 in the
carrier of
C )
and A84:
i = [o1,o2]
by ZFMISC_1:84;
reconsider o1 =
o1,
o2 =
o2 as
Object of
C by A83;
thus
the
Arrows of
S1 . i = the
Arrows of
S2 . i
verumproof
thus
the
Arrows of
S1 . i c= the
Arrows of
S2 . i
XBOOLE_0:def 10 the Arrows of S2 . i c= the Arrows of S1 . iproof
let n be
object ;
TARSKI:def 3 ( not n in the Arrows of S1 . i or n in the Arrows of S2 . i )
assume A85:
n in the
Arrows of
S1 . i
;
n in the Arrows of S2 . i
the
Arrows of
S1 . i c= the
Arrows of
C . i
by A76, A77, A82;
then reconsider m =
n as
Morphism of
o1,
o2 by A84, A85;
A86:
m in the
Arrows of
S1 . (
o1,
o2)
by A84, A85;
then A87:
m is
retraction
by A78;
(
<^o1,o2^> <> {} &
<^o2,o1^> <> {} )
by A78, A86;
then
m in the
Arrows of
S2 . (
o1,
o2)
by A81, A87;
hence
n in the
Arrows of
S2 . i
by A84;
verum
end;
let n be
object ;
TARSKI:def 3 ( not n in the Arrows of S2 . i or n in the Arrows of S1 . i )
assume A88:
n in the
Arrows of
S2 . i
;
n in the Arrows of S1 . i
the
Arrows of
S2 . i c= the
Arrows of
C . i
by A79, A80, A82;
then reconsider m =
n as
Morphism of
o1,
o2 by A84, A88;
A89:
m in the
Arrows of
S2 . (
o1,
o2)
by A84, A88;
then A90:
m is
retraction
by A81;
(
<^o1,o2^> <> {} &
<^o2,o1^> <> {} )
by A81, A89;
then
m in the
Arrows of
S1 . (
o1,
o2)
by A78, A90;
hence
n in the
Arrows of
S1 . i
by A84;
verum
end; end;
hence
S1 = S2
by A76, A79, ALTCAT_2:26, PBOOLE:3; verum