ex B being non empty strict subcategory of W -SUP_category st
( ( for a being Object of (W -SUP_category) holds
( a is Object of B iff S1[a] ) ) & ( for a, b being Object of (W -SUP_category)
for a9, b9 being Object of B st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S2[a,b,f] ) ) )
from YELLOW18:sch 7(A2, A3, A12);
hence
ex b1 being non empty strict subcategory of W -SUP_category st
( ( for a being Object of (W -SUP_category) holds a is Object of b1 ) & ( for a, b being Object of (W -SUP_category)
for a9, b9 being Object of b1 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) )
; verum