let A be non empty Poset; :: thesis: for f being Choice_Function of (BOOL the carrier of A) holds {(f . the carrier of A)} is Chain of f
let f be Choice_Function of (BOOL the carrier of A); :: thesis: {(f . the carrier of A)} is Chain of f
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;
A1: the InternalRel of A is_well_founded_in X
proof
reconsider x = aa as set ;
let Y be set ; :: according to WELLORD1:def 3 :: thesis: ( not Y c= X or Y = {} or ex b1 being object st
( b1 in Y & the InternalRel of A -Seg b1 misses Y ) )
assume that
A2: Y c= X and
A3: Y <> {} ; :: thesis: ex b1 being object st
( b1 in Y & the InternalRel of A -Seg b1 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;
A6: for a being Element of A st a in X holds
f . (UpperCone (InitSegm (X,a))) = a
proof
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 A7: 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 A8: x in (LowerCone {a}) /\ X ; :: thesis: x in {} A
then x in LowerCone {a} by XBOOLE_0:def 4;
then A9: 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 A8, XBOOLE_0:def 4;
hence x in {} A by A7, A9; :: thesis: verum
end;
then (LowerCone {a}) /\ X = {} A ;
hence f . (UpperCone (InitSegm (X,a))) = a by A7, Th14; :: thesis: verum
end;
the InternalRel of A is_strongly_connected_in X by Def7;
then A10: the InternalRel of A is_connected_in X ;
the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
then A11: the InternalRel of A is_antisymmetric_in X ;
the InternalRel of A is_transitive_in the carrier of A by Def3;
then A12: the InternalRel of A is_transitive_in X ;
the InternalRel of A is_reflexive_in the carrier of A by Def2;
then the InternalRel of A is_reflexive_in X ;
then the InternalRel of A well_orders X by A12, A11, A10, A1;
hence {(f . the carrier of A)} is Chain of f by A6, Def12; :: thesis: verum