let A be non empty Poset; :: thesis: for S, T being Subset of A st S c= T & the InternalRel of A well_orders T & ( for a1, a2 being Element of A st a2 in S & a1 in T & a1 < a2 holds
a1 in S ) & not S = T holds
S is Initial_Segm of T
let S, T be Subset of A; :: thesis: ( S c= T & the InternalRel of A well_orders T & ( for a1, a2 being Element of A st a2 in S & a1 in T & a1 < a2 holds
a1 in S ) & not S = T implies S is Initial_Segm of T )
assume that
A1: S c= T and
A2: the InternalRel of A well_orders T and
A3: for a1, a2 being Element of A st a2 in S & a1 in T & a1 < a2 holds
a1 in S and
A4: S <> T ; :: thesis: S is Initial_Segm of T

per cases ( T <> {} or T = {} ) ;
:: according to ORDERS_2:def 11

case T <> {} ; :: thesis: ex a being Element of A st
( a in T & S = InitSegm (T,a) )

set Y = T \ S;
not T c= S by A1, A4;
then T \ S <> {} by XBOOLE_1:37;
then consider x being object such that
A5: x in T \ S and
A6: for y being object st y in T \ S holds
[x,y] in the InternalRel of A by A2, WELLORD1:5, XBOOLE_1:36;
reconsider x = x as Element of A by A5;
take x ; :: thesis: ( x in T & S = InitSegm (T,x) )
thus A7: x in T by A5, XBOOLE_0:def 5; :: thesis: S = InitSegm (T,x)
S = (LowerCone {x}) /\ T

proof

thus S c= (LowerCone {x}) /\ T :: according to XBOOLE_0:def 10 :: thesis: (LowerCone {x}) /\ T c= S

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in S or y in (LowerCone {x}) /\ T )
assume A8: y in S ; :: thesis: y in (LowerCone {x}) /\ T
then reconsider a = y as Element of A ;

now :: thesis: for a1 being Element of A st a1 in {x} holds
a < a1

let a1 be Element of A; :: thesis: ( a1 in {x} implies a < a1 )
assume that
A9: a1 in {x} and
A10: not a < a1 ; :: thesis: contradiction
A11: a1 = x by A9, TARSKI:def 1;
then A12: a1 <> a by A5, A8, XBOOLE_0:def 5;
T is Chain of A by A2, Th13;
then a1 <= a by A1, A7, A8, A10, A11, Th12;
then a1 < a by A12;
then a1 in S by A3, A7, A8, A11;
hence contradiction by A5, A11, XBOOLE_0:def 5; :: thesis: verum

end;

then y in { a1 where a1 is Element of A : for a2 being Element of A st a2 in {x} holds
a1 < a2 } ;
hence y in (LowerCone {x}) /\ T by A1, A8, XBOOLE_0:def 4; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (LowerCone {x}) /\ T or y in S )
assume A13: y in (LowerCone {x}) /\ T ; :: thesis: y in S
then y in LowerCone {x} by XBOOLE_0:def 4;
then consider a being Element of A such that
A14: a = y and
A15: for a2 being Element of A st a2 in {x} holds
a < a2 ;

A16: now :: thesis: not y in T \ S

assume y in T \ S ; :: thesis: contradiction
then [x,y] in the InternalRel of A by A6;
then A17: x <= a by A14;
x in {x} by TARSKI:def 1;
hence contradiction by A15, A17, Th6; :: thesis: verum

end;

y in T by A13, XBOOLE_0:def 4;
hence y in S by A16, XBOOLE_0:def 5; :: thesis: verum

end;

hence S = InitSegm (T,x) ; :: thesis: verum

end;

case T = {} ; :: thesis: S = {}

hence S = {} by A1; :: thesis: verum

end;

end;