let C be non empty AltCatStr ; :: thesis: for D being non empty SubCatStr of C
for o1, o2 being object of
for p1, p2 being object of st o1 = p1 & o2 = p2 & <^p1,p2^> <> {} holds
for n being Morphism of , holds n is Morphism of ,
let D be non empty SubCatStr of C; :: thesis: for o1, o2 being object of
for p1, p2 being object of st o1 = p1 & o2 = p2 & <^p1,p2^> <> {} holds
for n being Morphism of , holds n is Morphism of ,
let o1, o2 be object of ; :: thesis: for p1, p2 being object of st o1 = p1 & o2 = p2 & <^p1,p2^> <> {} holds
for n being Morphism of , holds n is Morphism of ,
let p1, p2 be object of ; :: thesis: ( o1 = p1 & o2 = p2 & <^p1,p2^> <> {} implies for n being Morphism of , holds n is Morphism of , )
assume A1: ( o1 = p1 & o2 = p2 & <^p1,p2^> <> {} ) ; :: thesis: for n being Morphism of , holds n is Morphism of ,
let n be Morphism of ,; :: thesis: n is Morphism of ,
( n in <^p1,p2^> & <^p1,p2^> c= <^o1,o2^> ) by A1, Th32;
hence n is Morphism of , ; :: thesis: verum