let A be non empty Poset; :: thesis:
let f be Choice_Function of BOOL the carrier of A; :: thesis:
let fC1, fC2 be Chain of f; :: thesis:
assume A1: fC1 <> fC2 ; :: thesis:
set N = { a where a is Element of A : ( a in fC1 /\ fC2 & InitSegm fC1,a = InitSegm fC2,a ) } ;
A2: { a where a is Element of A : ( a in fC1 /\ fC2 & InitSegm fC1,a = InitSegm fC2,a ) } c= fC1

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { a where a is Element of A : ( a in fC1 /\ fC2 & InitSegm fC1,a = InitSegm fC2,a ) } ; :: thesis:
then ex a being Element of A st
( a = x & a in fC1 /\ fC2 & InitSegm fC1,a = InitSegm fC2,a ) ;
hence x in fC1 by XBOOLE_0:def 4; :: thesis:

end;

then reconsider N = { a where a is Element of A : ( a in fC1 /\ fC2 & InitSegm fC1,a = InitSegm fC2,a ) } as Subset of A by XBOOLE_1:1;
A3: the InternalRel of A well_orders fC1 by Def16;

A4: now

let a1, a2 be Element of A; :: thesis:
assume that
A5: a2 in N and
A6: a1 in fC1 and
A7: a1 < a2 ; :: thesis:
A8: ex a being Element of A st
( a = a2 & a in fC1 /\ fC2 & InitSegm fC1,a = InitSegm fC2,a ) by A5;
then a1 in InitSegm fC2,a2 by A6, A7, Th57;
then a1 in fC2 by XBOOLE_0:def 4;
then A9: a1 in fC1 /\ fC2 by A6, XBOOLE_0:def 4;
InitSegm fC1,a1 = InitSegm fC2,a1

thus InitSegm fC1,a1 c= InitSegm fC2,a1 :: according to XBOOLE_0:def 10 :: thesis:

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A10: x in InitSegm fC1,a1 ; :: thesis:
then reconsider b = x as Element of A ;
A11: b < a1 by A10, Th57;
then ( b < a2 & b in fC1 ) by A7, A10, Th29, Th57;
then b in InitSegm fC1,a2 by Th57;
then b in fC2 by A8, Th57;
hence x in InitSegm fC2,a1 by A11, Th57; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A12: x in InitSegm fC2,a1 ; :: thesis:
then reconsider b = x as Element of A ;
A13: b < a1 by A12, Th57;
then ( b < a2 & b in fC2 ) by A7, A12, Th29, Th57;
then b in InitSegm fC2,a2 by Th57;
then b in fC1 by A8, Th57;
hence x in InitSegm fC1,a1 by A13, Th57; :: thesis:

end;

hence a1 in N by A9; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in N ; :: thesis:
then ex a being Element of A st
( a = x & a in fC1 /\ fC2 & InitSegm fC1,a = InitSegm fC2,a ) ;
hence x in fC2 by XBOOLE_0:def 4; :: thesis:

end;

A16: now

let a1, a2 be Element of A; :: thesis:
assume that
A17: a2 in N and
A18: a1 in fC2 and
A19: a1 < a2 ; :: thesis:
A20: ex a being Element of A st
( a = a2 & a in fC1 /\ fC2 & InitSegm fC1,a = InitSegm fC2,a ) by A17;
then a1 in InitSegm fC1,a2 by A18, A19, Th57;
then a1 in fC1 by XBOOLE_0:def 4;
then A21: a1 in fC1 /\ fC2 by A18, XBOOLE_0:def 4;
InitSegm fC1,a1 = InitSegm fC2,a1

thus InitSegm fC1,a1 c= InitSegm fC2,a1 :: according to XBOOLE_0:def 10 :: thesis:

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A22: x in InitSegm fC1,a1 ; :: thesis:
then reconsider b = x as Element of A ;
A23: b < a1 by A22, Th57;
then ( b < a2 & b in fC1 ) by A19, A22, Th29, Th57;
then b in InitSegm fC1,a2 by Th57;
then b in fC2 by A20, Th57;
hence x in InitSegm fC2,a1 by A23, Th57; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A24: x in InitSegm fC2,a1 ; :: thesis:
then reconsider b = x as Element of A ;
A25: b < a1 by A24, Th57;
then ( b < a2 & b in fC2 ) by A19, A24, Th29, Th57;
then b in InitSegm fC2,a2 by Th57;
then b in fC1 by A20, Th57;
hence x in InitSegm fC1,a1 by A25, Th57; :: thesis:

end;

hence a1 in N by A21; :: thesis:

end;

now

per cases by A2, A3, A4, A14, A15, A16, Th73;

suppose ( N is Initial_Segm of fC1 & N = fC2 ) ; :: thesis:

then ( fC2 is Initial_Segm of fC1 & fC1 <> {} ) by Def16;
hence ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 ) by Th69; :: thesis:

end;

suppose ( N is Initial_Segm of fC2 & N = fC1 ) ; :: thesis:

then ( fC1 is Initial_Segm of fC2 & fC2 <> {} ) by Def16;
hence ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 ) by Th69; :: thesis:

end;

suppose ( N = fC1 & N = fC2 ) ; :: thesis:

hence ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 ) by A1; :: thesis:

end;

suppose A26: ( N is Initial_Segm of fC1 & N is Initial_Segm of fC2 ) ; :: thesis:

fC1 <> {} by Def16;
then consider a being Element of A such that
A27: a in fC1 and
A28: N = InitSegm fC1,a by A26, Def15;
fC2 <> {} by Def16;
then consider b being Element of A such that
A29: b in fC2 and
A30: N = InitSegm fC2,b by A26, Def15;
A31: a = f . (UpperCone (InitSegm fC2,b)) by A27, A28, A30, Def16
.= b by A29, Def16 ;
then a in fC1 /\ fC2 by A27, A29, XBOOLE_0:def 4;
then a in N by A28, A30, A31;
hence ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 ) by A28, Th62; :: thesis:

end;

hence ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 ) ; :: thesis: