now

consider x being Element of S;
assume S <> {} ; :: thesis: ex T being Subset of st
( ( S <> {} implies ex a being Element of st
( a in S & T = InitSegm S,a ) ) & ( S = {} implies T = {} ) )
then reconsider x = x as Element of by Lm1;
take T = InitSegm S,x; :: thesis: ( ( S <> {} implies ex a being Element of st
( a in S & T = InitSegm S,a ) ) & ( S = {} implies T = {} ) )
thus ( S <> {} implies ex a being Element of st
( a in S & T = InitSegm S,a ) ) ; :: thesis: ( S = {} implies T = {} )
thus ( S = {} implies T = {} ) ; :: thesis: verum

end;

hence ( ( S <> {} implies ex b₁ being Subset of ex a being Element of st
( a in S & b₁ = InitSegm S,a ) ) & ( not S <> {} implies ex b₁ being Subset of st b₁ = {} ) ) ; :: thesis: verum