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 iso ) ) ) & 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 iso ) ) ) implies S1 = S2 )
assume that
A73:
the carrier of S1 = the carrier of C
and
A74:
the Arrows of S1 cc= the Arrows of C
and
A75:
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 iso ) )
and
A76:
the carrier of S2 = the carrier of C
and
A77:
the Arrows of S2 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 S2 . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is iso ) )
; S1 = S2
now let i be
set ;
( i in [: the carrier of C, the carrier of C:] implies the Arrows of S1 . i = the Arrows of S2 . i )assume A79:
i in [: the carrier of C, the carrier of C:]
;
the Arrows of S1 . i = the Arrows of S2 . ithen consider o1,
o2 being
set such that A80:
(
o1 in the
carrier of
C &
o2 in the
carrier of
C )
and A81:
i = [o1,o2]
by ZFMISC_1:84;
reconsider o1 =
o1,
o2 =
o2 as
object of
C by A80;
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
set ;
TARSKI:def 3 ( not n in the Arrows of S1 . i or n in the Arrows of S2 . i )
assume A82:
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 A73, A74, A79, ALTCAT_2:def 2;
then reconsider m =
n as
Morphism of
o1,
o2 by A81, A82;
A83:
m in the
Arrows of
S1 . (
o1,
o2)
by A81, A82;
then A84:
m is
iso
by A75;
(
<^o1,o2^> <> {} &
<^o2,o1^> <> {} )
by A75, A83;
then
m in the
Arrows of
S2 . (
o1,
o2)
by A78, A84;
hence
n in the
Arrows of
S2 . i
by A81;
verum
end;
let n be
set ;
TARSKI:def 3 ( not n in the Arrows of S2 . i or n in the Arrows of S1 . i )
assume A85:
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 A76, A77, A79, ALTCAT_2:def 2;
then reconsider m =
n as
Morphism of
o1,
o2 by A81, A85;
A86:
m in the
Arrows of
S2 . (
o1,
o2)
by A81, A85;
then A87:
m is
iso
by A78;
(
<^o1,o2^> <> {} &
<^o2,o1^> <> {} )
by A78, A86;
then
m in the
Arrows of
S1 . (
o1,
o2)
by A75, A87;
hence
n in the
Arrows of
S1 . i
by A81;
verum
end; end;
hence
S1 = S2
by A73, A76, ALTCAT_2:26, PBOOLE:3; verum