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 < 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 < 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 < 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 15

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, XBOOLE_0:def 10;
then ( T \ S c= T & T \ S <> {} ) by XBOOLE_1:36, XBOOLE_1:37;
then consider x being set such that
A5: x in T \ S and
A6: for y being set st y in T \ S holds
[x,y] in the InternalRel of A by A2, WELLORD1:9;
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 set ; :: 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

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: ( T is Chain of A & a1 = x ) by A2, A9, Th40, TARSKI:def 1;
then ( a1 <= a & a1 <> a ) by A1, A5, A7, A8, A10, Th39, XBOOLE_0:def 5;
then a1 < a by Def10;
then a1 in S by A3, A8;
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 set ; :: according to TARSKI:def 3 :: thesis: ( not y in (LowerCone {x}) /\ T or y in S )
assume A12: 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
A13: a = y and
A14: for a2 being Element of A st a2 in {x} holds
a < a2 ;

A15: now

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

end;

y in T by A12, XBOOLE_0:def 4;
hence y in S by A15, 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;