let S1, S2 be non empty transitive strict SubCatStr of C; :: thesis: ( 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 coretraction ) ) ) & 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 coretraction ) ) ) implies S1 = S2 )
assume that
A51:
the carrier of S1 = the carrier of C
and
A52:
the Arrows of S1 cc= the Arrows of C
and
A53:
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 coretraction ) )
and
A54:
the carrier of S2 = the carrier of C
and
A55:
the Arrows of S2 cc= the Arrows of C
and
A56:
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 coretraction ) )
; :: thesis: S1 = S2
now let i be
set ;
:: thesis: ( i in [:the carrier of C,the carrier of C:] implies the Arrows of S1 . i = the Arrows of S2 . i )assume A57:
i in [:the carrier of C,the carrier of C:]
;
:: thesis: the Arrows of S1 . i = the Arrows of S2 . ithen consider o1,
o2 being
set such that A58:
(
o1 in the
carrier of
C &
o2 in the
carrier of
C &
i = [o1,o2] )
by ZFMISC_1:103;
reconsider o1 =
o1,
o2 =
o2 as
object of
C by A58;
thus
the
Arrows of
S1 . i = the
Arrows of
S2 . i
:: thesis: verumproof
thus
the
Arrows of
S1 . i c= the
Arrows of
S2 . i
:: according to XBOOLE_0:def 10 :: thesis: the Arrows of S2 . i c= the Arrows of S1 . iproof
let n be
set ;
:: according to TARSKI:def 3 :: thesis: ( not n in the Arrows of S1 . i or n in the Arrows of S2 . i )
assume A59:
n in the
Arrows of
S1 . i
;
:: thesis: n in the Arrows of S2 . i
the
Arrows of
S1 . i c= the
Arrows of
C . i
by A51, A52, A57, ALTCAT_2:def 2;
then reconsider m =
n as
Morphism of
o1,
o2 by A58, A59;
m in the
Arrows of
S1 . o1,
o2
by A58, A59;
then
(
<^o1,o2^> <> {} &
<^o2,o1^> <> {} &
m is
coretraction )
by A53;
then
m in the
Arrows of
S2 . o1,
o2
by A56;
hence
n in the
Arrows of
S2 . i
by A58;
:: thesis: verum
end;
let n be
set ;
:: according to TARSKI:def 3 :: thesis: ( not n in the Arrows of S2 . i or n in the Arrows of S1 . i )
assume A60:
n in the
Arrows of
S2 . i
;
:: thesis: n in the Arrows of S1 . i
the
Arrows of
S2 . i c= the
Arrows of
C . i
by A54, A55, A57, ALTCAT_2:def 2;
then reconsider m =
n as
Morphism of
o1,
o2 by A58, A60;
m in the
Arrows of
S2 . o1,
o2
by A58, A60;
then
(
<^o1,o2^> <> {} &
<^o2,o1^> <> {} &
m is
coretraction )
by A56;
then
m in the
Arrows of
S1 . o1,
o2
by A53;
hence
n in the
Arrows of
S1 . i
by A58;
:: thesis: verum
end; end;
hence
S1 = S2
by A51, A54, ALTCAT_2:27, PBOOLE:3; :: thesis: verum