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;