RelStr(# a, the well-ordering upper-bounded Order of a #) is Object of (W -SUP_category) by A1, Def5;
then reconsider b = RelStr(# a, the well-ordering upper-bounded Order of a #) as Object of (W -SUP(SO)_category) by Def11;
b = latt b ;
then A2: ex b being Object of (W -SUP(SO)_category) st S₁[b] ;
thus ex B being non empty strict full subcategory of W -SUP(SO)_category st
for a being Object of (W -SUP(SO)_category) holds
( a is Object of B iff S₁[a] ) from YELLOW20:sch 2(A2); :: thesis: verum