now :: thesis: ( S <> {} implies ex T being Subset of A st
( ( S <> {} implies ex a being Element of A st
( a in S & T = InitSegm (S,a) ) ) & ( S = {} implies T = {} ) ) )

set x = the Element of S;
assume S <> {} ; :: thesis: ex T being Subset of A st
( ( S <> {} implies ex a being Element of A st
( a in S & T = InitSegm (S,a) ) ) & ( S = {} implies T = {} ) )
then reconsider x = the Element of S as Element of A by Lm1;
take T = InitSegm (S,x); :: thesis: ( ( S <> {} implies ex a being Element of A st
( a in S & T = InitSegm (S,a) ) ) & ( S = {} implies T = {} ) )
thus ( S <> {} implies ex a being Element of A 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 A ex a being Element of A st
( a in S & b₁ = InitSegm (S,a) ) ) & ( not S <> {} implies ex b₁ being Subset of A st b₁ = {} ) ) ; :: thesis: verum