reconsider b = RelStr(# a,r #) 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₁[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₁[a] ) from YELLOW20:sch 2(A2); :: thesis: verum