let B1, B2 be non empty strict full subcategory of W -UPS_category ; :: thesis: ( ( for a being Object of (W -UPS_category) holds

( a is Object of B1 iff latt a is continuous ) ) & ( for a being Object of (W -UPS_category) holds

( a is Object of B2 iff latt a is continuous ) ) implies B1 = B2 )

assume that

A3: for a being Object of (W -UPS_category) holds

( a is Object of B1 iff S_{1}[a] )
and

A4: for a being Object of (W -UPS_category) holds

( a is Object of B2 iff S_{1}[a] )
; :: thesis: B1 = B2

AltCatStr(# the carrier of B1, the Arrows of B1, the Comp of B1 #) = AltCatStr(# the carrier of B2, the Arrows of B2, the Comp of B2 #) from YELLOW20:sch 3(A3, A4);

hence B1 = B2 ; :: thesis: verum

( a is Object of B1 iff latt a is continuous ) ) & ( for a being Object of (W -UPS_category) holds

( a is Object of B2 iff latt a is continuous ) ) implies B1 = B2 )

assume that

A3: for a being Object of (W -UPS_category) holds

( a is Object of B1 iff S

A4: for a being Object of (W -UPS_category) holds

( a is Object of B2 iff S

AltCatStr(# the carrier of B1, the Arrows of B1, the Comp of B1 #) = AltCatStr(# the carrier of B2, the Arrows of B2, the Comp of B2 #) from YELLOW20:sch 3(A3, A4);

hence B1 = B2 ; :: thesis: verum