ex S being SetSequence of T st
( S is open & S is closed & ( not T is empty implies S is non-empty ) ) by Lm1;
hence ex b₁ being SetSequence of T st
( b₁ is open & b₁ is non-empty ) ; :: thesis: verum