let A be non empty Poset; :: thesis: for S being Subset of A
for I being Initial_Segm of S holds I c= S
let S be Subset of A; :: thesis: for I being Initial_Segm of S holds I c= S
let I be Initial_Segm of S; :: thesis: I c= S

per cases ( S = {} or S <> {} ) ;

suppose S = {} ; :: thesis: I c= S

hence I c= S by Def15; :: thesis: verum

end;

suppose S <> {} ; :: thesis: I c= S

then consider a being Element of A such that
a in S and
A1: I = InitSegm S,a by Def15;
thus I c= S by A1, XBOOLE_1:17; :: thesis: verum

end;

end;