let A be non empty Poset; 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; ( 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
; S is Initial_Segm of T
per cases
( T <> {} or T = {} )
;
ORDERS_2:def 11case
T <> {}
;
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
;
( x in T & S = InitSegm (T,x) )thus A7:
x in T
by A5, XBOOLE_0:def 5;
S = InitSegm (T,x)
S = (LowerCone {x}) /\ T
proof
thus
S c= (LowerCone {x}) /\ T
XBOOLE_0:def 10 (LowerCone {x}) /\ T c= Sproof
let y be
object ;
TARSKI:def 3 ( not y in S or y in (LowerCone {x}) /\ T )
assume A8:
y in S
;
y in (LowerCone {x}) /\ T
then reconsider a =
y as
Element of
A ;
now for a1 being Element of A st a1 in {x} holds
a < a1let a1 be
Element of
A;
( a1 in {x} implies a < a1 )assume that A9:
a1 in {x}
and A10:
not
a < a1
;
contradictionA11:
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, A8;
hence
contradiction
by A5, A11, XBOOLE_0:def 5;
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;
verum
end;
let y be
object ;
TARSKI:def 3 ( not y in (LowerCone {x}) /\ T or y in S )
assume A13:
y in (LowerCone {x}) /\ T
;
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
;
y in T
by A13, XBOOLE_0:def 4;
hence
y in S
by A16, XBOOLE_0:def 5;
verum
end; hence
S = InitSegm (
T,
x)
;
verum end;