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

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

end;

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

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

end;

end;

end;

hence contradiction ; :: thesis: verum