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