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

end;

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

then ex a being Element of A st
( a in S & I = InitSegm (S,a) ) by Def11;
hence I c= S by XBOOLE_1:17; :: thesis: verum

end;

end;