consider T being non empty non trivial strict anti-discrete TopSpace;
consider B being 2nd_class Subset of T;
B is 2nd_class ;
then A1: T is with_2nd_class_subsets by Def10;
{} T is 1st_class ;
then T is with_1st_class_subsets by Def9;
hence ex b₁ being TopSpace st
( b₁ is with_1st_class_subsets & b₁ is with_2nd_class_subsets & not b₁ is empty & b₁ is strict & not b₁ is trivial ) by A1; :: thesis: verum