let B1, B2 be non empty strict subcategory of W -INF_category ; :: thesis: ( ( for a being object of (W -INF_category ) holds a is object of B1 ) & ( for a, b being object of (W -INF_category )
for a9, b9 being object of B1 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) & ( for a being object of (W -INF_category ) holds a is object of B2 ) & ( for a, b being object of (W -INF_category )
for a9, b9 being object of B2 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) implies B1 = B2 )
assume for a being object of (W -INF_category ) holds a is object of B1 ; :: thesis: ( ex a, b being object of (W -INF_category ) ex a9, b9 being object of B1 st
( a9 = a & b9 = b & <^a,b^> <> {} & not for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) or ex a being object of (W -INF_category ) st a is not object of B2 or ex a, b being object of (W -INF_category ) ex a9, b9 being object of B2 st
( a9 = a & b9 = b & <^a,b^> <> {} & not for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) or B1 = B2 )
then A9: for a being object of (W -INF_category ) holds
( a is object of B1 iff S₁[a] ) ;
assume A10: for a, b being object of (W -INF_category )
for a9, b9 being object of B1 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S₂[a,b,f] ) ; :: thesis: ( ex a being object of (W -INF_category ) st a is not object of B2 or ex a, b being object of (W -INF_category ) ex a9, b9 being object of B2 st
( a9 = a & b9 = b & <^a,b^> <> {} & not for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) or B1 = B2 )
assume for a being object of (W -INF_category ) holds a is object of B2 ; :: thesis: ( ex a, b being object of (W -INF_category ) ex a9, b9 being object of B2 st
( a9 = a & b9 = b & <^a,b^> <> {} & not for f being Morphism of a,b holds
( f in <^a9,b9^> iff @ f is directed-sups-preserving ) ) or B1 = B2 )
then A11: for a being object of (W -INF_category ) holds
( a is object of B2 iff S₁[a] ) ;
assume A12: for a, b being object of (W -INF_category )
for a9, b9 being object of B2 st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S₂[a,b,f] ) ; :: 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 1(A9, A10, A11, A12);
hence B1 = B2 ; :: thesis: verum