let B1, B2 be non empty strict full subcategory of W -INF(SC)_category ; :: thesis: ( ( for a being object of (W -INF(SC)_category ) holds
( a is object of B1 iff latt a is continuous ) ) & ( for a being object of (W -INF(SC)_category ) holds
( a is object of B2 iff latt a is continuous ) ) implies B1 = B2 )
assume that
A3: for a being object of (W -INF(SC)_category ) holds
( a is object of B1 iff S₁[a] ) and
A4: for a being object of (W -INF(SC)_category ) holds
( a is object of B2 iff S₁[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