set AC = the carrier of A;
( the carrier of A in BOOL the carrier of A & not {} in BOOL the carrier of A ) by ORDERS_1:1, ORDERS_1:2;
then reconsider aa = f . the carrier of A as Element of A by ORDERS_1:89;
reconsider X = {aa} as Chain of A by Th8;
take X ; :: thesis: ( X <> {} & the InternalRel of A well_orders X & ( for a being Element of A st a in X holds
f . (UpperCone (InitSegm (X,a))) = a ) )
thus X <> {} ; :: thesis: ( the InternalRel of A well_orders X & ( for a being Element of A st a in X holds
f . (UpperCone (InitSegm (X,a))) = a ) )
A1: the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
( the InternalRel of A is_reflexive_in the carrier of A & the InternalRel of A is_transitive_in the carrier of A ) by Def2, Def3;
hence ( the InternalRel of A is_reflexive_in X & the InternalRel of A is_transitive_in X & the InternalRel of A is_antisymmetric_in X ) by A1; :: according to WELLORD1:def 5 :: thesis: ( the InternalRel of A is_connected_in X & the InternalRel of A is_well_founded_in X & ( for a being Element of A st a in X holds
f . (UpperCone (InitSegm (X,a))) = a ) )
the InternalRel of A is_strongly_connected_in X by Def7;
hence the InternalRel of A is_connected_in X ; :: thesis: ( the InternalRel of A is_well_founded_in X & ( for a being Element of A st a in X holds
f . (UpperCone (InitSegm (X,a))) = a ) )
thus the InternalRel of A is_well_founded_in X :: thesis: for a being Element of A st a in X holds
f . (UpperCone (InitSegm (X,a))) = a

proof

reconsider x = aa as set ;
let Y be set ; :: according to WELLORD1:def 3 :: thesis: ( not Y c= X or Y = {} or ex b₁ being object st
( b₁ in Y & the InternalRel of A -Seg b₁ misses Y ) )
assume that
A2: Y c= X and
A3: Y <> {} ; :: thesis: ex b₁ being object st
( b₁ in Y & the InternalRel of A -Seg b₁ misses Y )
take x ; :: thesis: ( x in Y & the InternalRel of A -Seg x misses Y )
Y = X by A2, A3, ZFMISC_1:33;
hence x in Y by TARSKI:def 1; :: thesis: the InternalRel of A -Seg x misses Y
thus ( the InternalRel of A -Seg x) /\ Y c= {} :: according to XBOOLE_0:def 7,XBOOLE_0:def 10 :: thesis: {} c= ( the InternalRel of A -Seg x) /\ Y

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in ( the InternalRel of A -Seg x) /\ Y or y in {} )
assume A4: y in ( the InternalRel of A -Seg x) /\ Y ; :: thesis: y in {}
then y in Y by XBOOLE_0:def 4;
then A5: y = aa by A2, TARSKI:def 1;
y in the InternalRel of A -Seg x by A4, XBOOLE_0:def 4;
hence y in {} by A5, WELLORD1:1; :: thesis: verum

end;

thus {} c= ( the InternalRel of A -Seg x) /\ Y ; :: thesis: verum

end;

let a be Element of A; :: thesis: ( a in X implies f . (UpperCone (InitSegm (X,a))) = a )
assume a in X ; :: thesis: f . (UpperCone (InitSegm (X,a))) = a
then A6: a = aa by TARSKI:def 1;
(LowerCone {a}) /\ X c= {} A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (LowerCone {a}) /\ X or x in {} A )
assume A7: x in (LowerCone {a}) /\ X ; :: thesis: x in {} A
then x in LowerCone {a} by XBOOLE_0:def 4;
then A8: ex a1 being Element of A st
( x = a1 & ( for a2 being Element of A st a2 in {a} holds
a1 < a2 ) ) ;
x in X by A7, XBOOLE_0:def 4;
hence x in {} A by A6, A8; :: thesis: verum

end;

then (LowerCone {a}) /\ X = {} A ;
hence f . (UpperCone (InitSegm (X,a))) = a by A6, Th14; :: thesis: verum