reconsider b = RelStr(# a, the well-ordering upper-bounded Order of a #) as Object of (W -UPS_category) by A1, Def10;

b = latt b ;

then reconsider b = b as Object of (W -CONT_category) by Def11;

b = latt b ;

then A2: ex b being Object of (W -CONT_category) st S_{1}[b]
;

thus ex C being non empty strict full subcategory of W -CONT_category st

for a being Object of (W -CONT_category) holds

( a is Object of C iff S_{1}[a] )
from YELLOW20:sch 2(A2); :: thesis: verum

b = latt b ;

then reconsider b = b as Object of (W -CONT_category) by Def11;

b = latt b ;

then A2: ex b being Object of (W -CONT_category) st S

thus ex C being non empty strict full subcategory of W -CONT_category st

for a being Object of (W -CONT_category) holds

( a is Object of C iff S