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