ex B being non empty strict subcategory of non empty strict st
( ( for a being object of holds
( a is object of iff S₁[a] ) ) & ( 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] ) ) ) from YELLOW18:sch 7(A2, A3, A12);
hence ex b₁ being non empty strict subcategory of non empty strict st
( ( 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 ) ) ) ; :: thesis: verum