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 closed ; :: thesis: verum