let A be non empty Poset; :: thesis: for f being Choice_Function of (BOOL the carrier of A)
for fC1, fC2 being Chain of f st fC1 <> fC2 holds
( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
let f be Choice_Function of (BOOL the carrier of A); :: thesis: for fC1, fC2 being Chain of f st fC1 <> fC2 holds
( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
let fC1, fC2 be Chain of f; :: thesis: ( fC1 <> fC2 implies ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 ) )
assume A1: fC1 <> fC2 ; :: thesis: ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
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
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { a where a is Element of A : ( a in fC1 /\ fC2 & InitSegm (fC1,a) = InitSegm (fC2,a) ) } or x in fC1 )
assume x in { a where a is Element of A : ( a in fC1 /\ fC2 & InitSegm (fC1,a) = InitSegm (fC2,a) ) } ; :: thesis: x in fC1
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: verum
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: N c= fC2
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N or x in fC2 )
assume x in N ; :: thesis: x in fC2
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: verum
end;
A4: now :: thesis: for a1, a2 being Element of A st a2 in N & a1 in fC1 & a1 < a2 holds
a1 in N
let a1, a2 be Element of A; :: thesis: ( a2 in N & a1 in fC1 & a1 < a2 implies a1 in N )
assume that
A5: a2 in N and
A6: a1 in fC1 and
A7: a1 < a2 ; :: thesis: a1 in N
A8: ex a being Element of A st
( a = a2 & a in fC1 /\ fC2 & InitSegm (fC1,a) = InitSegm (fC2,a) ) by A5;
A9: InitSegm (fC1,a1) = InitSegm (fC2,a1)
proof
thus InitSegm (fC1,a1) c= InitSegm (fC2,a1) :: according to XBOOLE_0:def 10 :: thesis: InitSegm (fC2,a1) c= InitSegm (fC1,a1)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in InitSegm (fC1,a1) or x in InitSegm (fC2,a1) )
assume A10: x in InitSegm (fC1,a1) ; :: thesis: x in InitSegm (fC2,a1)
then reconsider b = x as Element of A ;
A11: b in fC1 by A10, Th24;
A12: b < a1 by A10, Th24;
then b < a2 by A7, Th5;
then b in InitSegm (fC1,a2) by A11, Th24;
then b in fC2 by A8, Th24;
hence x in InitSegm (fC2,a1) by A12, Th24; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in InitSegm (fC2,a1) or x in InitSegm (fC1,a1) )
assume A13: x in InitSegm (fC2,a1) ; :: thesis: x in InitSegm (fC1,a1)
then reconsider b = x as Element of A ;
A14: b in fC2 by A13, Th24;
A15: b < a1 by A13, Th24;
then b < a2 by A7, Th5;
then b in InitSegm (fC2,a2) by A14, Th24;
then b in fC1 by A8, Th24;
hence x in InitSegm (fC1,a1) by A15, Th24; :: thesis: verum
end;
a1 in InitSegm (fC2,a2) by A6, A7, A8, Th24;
then a1 in fC2 by XBOOLE_0:def 4;
then a1 in fC1 /\ fC2 by A6, XBOOLE_0:def 4;
hence a1 in N by A9; :: thesis: verum
end;
A16: now :: thesis: for a1, a2 being Element of A st a2 in N & a1 in fC2 & a1 < a2 holds
a1 in N
let a1, a2 be Element of A; :: thesis: ( a2 in N & a1 in fC2 & a1 < a2 implies a1 in N )
assume that
A17: a2 in N and
A18: a1 in fC2 and
A19: a1 < a2 ; :: thesis: a1 in N
A20: ex a being Element of A st
( a = a2 & a in fC1 /\ fC2 & InitSegm (fC1,a) = InitSegm (fC2,a) ) by A17;
A21: InitSegm (fC1,a1) = InitSegm (fC2,a1)
proof
thus InitSegm (fC1,a1) c= InitSegm (fC2,a1) :: according to XBOOLE_0:def 10 :: thesis: InitSegm (fC2,a1) c= InitSegm (fC1,a1)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in InitSegm (fC1,a1) or x in InitSegm (fC2,a1) )
assume A22: x in InitSegm (fC1,a1) ; :: thesis: x in InitSegm (fC2,a1)
then reconsider b = x as Element of A ;
A23: b in fC1 by A22, Th24;
A24: b < a1 by A22, Th24;
then b < a2 by A19, Th5;
then b in InitSegm (fC1,a2) by A23, Th24;
then b in fC2 by A20, Th24;
hence x in InitSegm (fC2,a1) by A24, Th24; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in InitSegm (fC2,a1) or x in InitSegm (fC1,a1) )
assume A25: x in InitSegm (fC2,a1) ; :: thesis: x in InitSegm (fC1,a1)
then reconsider b = x as Element of A ;
A26: b in fC2 by A25, Th24;
A27: b < a1 by A25, Th24;
then b < a2 by A19, Th5;
then b in InitSegm (fC2,a2) by A26, Th24;
then b in fC1 by A20, Th24;
hence x in InitSegm (fC1,a1) by A27, Th24; :: thesis: verum
end;
a1 in InitSegm (fC1,a2) by A18, A19, A20, Th24;
then a1 in fC1 by XBOOLE_0:def 4;
then a1 in fC1 /\ fC2 by A18, XBOOLE_0:def 4;
hence a1 in N by A21; :: thesis: verum
end;
A28: ( the InternalRel of A well_orders fC1 & the InternalRel of A well_orders fC2 ) by Def12;
now :: thesis: ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
per cases ( ( N is Initial_Segm of fC1 & N = fC2 ) or ( N is Initial_Segm of fC2 & N = fC1 ) or ( N = fC1 & N = fC2 ) or ( N is Initial_Segm of fC1 & N is Initial_Segm of fC2 ) ) by A2, A4, A28, A3, A16, Th35;
suppose A29: ( N is Initial_Segm of fC1 & N = fC2 ) ; :: thesis: ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
fC1 <> {} by Def12;
hence ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 ) by A29, Th31; :: thesis: verum
end;
suppose A30: ( N is Initial_Segm of fC2 & N = fC1 ) ; :: thesis: ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
fC2 <> {} by Def12;
hence ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 ) by A30, Th31; :: thesis: verum
end;
suppose ( N = fC1 & N = fC2 ) ; :: thesis: ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
hence ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 ) by A1; :: thesis: verum
end;
suppose A31: ( N is Initial_Segm of fC1 & N is Initial_Segm of fC2 ) ; :: thesis: ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
fC2 <> {} by Def12;
then consider b being Element of A such that
A32: b in fC2 and
A33: N = InitSegm (fC2,b) by A31, Def11;
fC1 <> {} by Def12;
then consider a being Element of A such that
A34: a in fC1 and
A35: N = InitSegm (fC1,a) by A31, Def11;
A36: a = f . (UpperCone (InitSegm (fC2,b))) by A34, A35, A33, Def12
.= b by A32, Def12 ;
then a in fC1 /\ fC2 by A34, A32, XBOOLE_0:def 4;
then a in N by A35, A33, A36;
hence ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 ) by A35, Th26; :: thesis: verum
end;
end;
end;
hence ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 ) ; :: thesis: verum