let A be non empty Poset; :: thesis: for S, T being Subset of A st S <> {} & S is Initial_Segm of T holds
not T is Initial_Segm of S
let S, T be Subset of A; :: thesis: ( S <> {} & S is Initial_Segm of T implies not T is Initial_Segm of S )
assume that
A1: S <> {} and
A2: S is Initial_Segm of T and
A3: T is Initial_Segm of S ; :: thesis: contradiction

now :: thesis: contradiction

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

suppose S = {} ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum

end;

suppose T = {} ; :: thesis: contradiction

hence contradiction by A1, A2, Def11; :: thesis: verum

end;

suppose A4: ( S <> {} & T <> {} ) ; :: thesis: contradiction

then consider a2 being Element of A such that
A5: a2 in T and
A6: S = InitSegm (T,a2) by A2, Def11;
consider a1 being Element of A such that
A7: a1 in S and
A8: T = InitSegm (S,a1) by A3, A4, Def11;
a1 in LowerCone {a2} by A7, A6, XBOOLE_0:def 4;
then A9: ex a being Element of A st
( a = a1 & ( for b being Element of A st b in {a2} holds
a < b ) ) ;
a2 in LowerCone {a1} by A8, A5, XBOOLE_0:def 4;
then A10: ex a3 being Element of A st
( a3 = a2 & ( for b being Element of A st b in {a1} holds
a3 < b ) ) ;
a1 in {a1} by TARSKI:def 1;
then A11: a2 < a1 by A10;
a2 in {a2} by TARSKI:def 1;
then a1 < a2 by A9;
hence contradiction by A11, Th4; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum