let B1, B2 be non empty strict subcategory of non empty strict ; :: thesis: ( ( for a being object of holds a is object of ) & ( for a, b being object of
for a', b' being object of st a' = a & b' = b & <^a,b^> <> {} holds
for f being Morphism of , holds
( f in <^a',b'^> iff UpperAdj (@ f) is directed-sups-preserving ) ) & ( for a being object of holds a is object of ) & ( for a, b being object of
for a', b' being object of st a' = a & b' = b & <^a,b^> <> {} holds
for f being Morphism of , holds
( f in <^a',b'^> iff UpperAdj (@ f) is directed-sups-preserving ) ) implies B1 = B2 )
assume for a being object of holds a is object of ; :: thesis: ( ex a, b being object of ex a', b' being object of st
( a' = a & b' = b & <^a,b^> <> {} & not for f being Morphism of , holds
( f in <^a',b'^> iff UpperAdj (@ f) is directed-sups-preserving ) ) or ex a being object of st a is not object of or ex a, b being object of ex a', b' being object of st
( a' = a & b' = b & <^a,b^> <> {} & not for f being Morphism of , holds
( f in <^a',b'^> iff UpperAdj (@ f) is directed-sups-preserving ) ) or B1 = B2 )
then A14: for a being object of holds
( a is object of iff S₁[a] ) ;
assume A15: for a, b being object of
for a', b' being object of st a' = a & b' = b & <^a,b^> <> {} holds
for f being Morphism of , holds
( f in <^a',b'^> iff S₂[a,b,f] ) ; :: thesis: ( ex a being object of st a is not object of or ex a, b being object of ex a', b' being object of st
( a' = a & b' = b & <^a,b^> <> {} & not for f being Morphism of , holds
( f in <^a',b'^> iff UpperAdj (@ f) is directed-sups-preserving ) ) or B1 = B2 )
assume for a being object of holds a is object of ; :: thesis: ( ex a, b being object of ex a', b' being object of st
( a' = a & b' = b & <^a,b^> <> {} & not for f being Morphism of , holds
( f in <^a',b'^> iff UpperAdj (@ f) is directed-sups-preserving ) ) or B1 = B2 )
then A16: for a being object of holds
( a is object of iff S₁[a] ) ;
assume A17: for a, b being object of
for a', b' being object of st a' = a & b' = b & <^a,b^> <> {} holds
for f being Morphism of , holds
( f in <^a',b'^> iff S₂[a,b,f] ) ; :: thesis: B1 = B2
AltCatStr(# the carrier of B1,the Arrows of B1,the Comp of B1 #) = AltCatStr(# the carrier of B2,the Arrows of B2,the Comp of B2 #) from YELLOW20:sch 1(A14, A15, A16, A17);
hence B1 = B2 ; :: thesis: verum