let C be non empty transitive AltCatStr ; for D being SubCatStr of C st the carrier of D = the carrier of C & the Arrows of D = the Arrows of C holds
AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #)
let D be SubCatStr of C; ( the carrier of D = the carrier of C & the Arrows of D = the Arrows of C implies AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) )
assume that
A1:
the carrier of D = the carrier of C
and
A2:
the Arrows of D = the Arrows of C
; AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #)
A3:
D is transitive
proof
let o1,
o2,
o3 be
Object of
D;
ALTCAT_1:def 2 ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
reconsider p1 =
o1,
p2 =
o2,
p3 =
o3 as
Object of
C by A1;
assume A4:
(
<^o1,o2^> <> {} &
<^o2,o3^> <> {} )
;
not <^o1,o3^> = {}
A5:
<^o1,o3^> = <^p1,p3^>
by A2;
(
<^o1,o2^> = <^p1,p2^> &
<^o2,o3^> = <^p2,p3^> )
by A2;
hence
not
<^o1,o3^> = {}
by A5, A4, ALTCAT_1:def 2;
verum
end;
A6:
C is SubCatStr of C
by Th20;
not D is empty
by A1;
then
C is SubCatStr of D
by A1, A2, A3, A6, Th24;
hence
AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #)
by Th22; verum