let i be Nat; :: thesis: for P being Subset of (TOP-REAL 2)
for f1, f2 being FinSequence of the carrier of (TOP-REAL 2) st f1,f2 are_generators_of P & 1 < i & i < len f1 holds
f1 /. i is_extremal_in P
let P be Subset of (TOP-REAL 2); :: thesis: for f1, f2 being FinSequence of the carrier of (TOP-REAL 2) st f1,f2 are_generators_of P & 1 < i & i < len f1 holds
f1 /. i is_extremal_in P
let f1, f2 be FinSequence of the carrier of (TOP-REAL 2); :: thesis: ( f1,f2 are_generators_of P & 1 < i & i < len f1 implies f1 /. i is_extremal_in P )
set p0 = f1 /. i;
set q1 = f1 /. 1;
set q2 = f1 /. (len f1);
set F1 = { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 ) } ;
set PP = union { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 ) } ;
reconsider u0 = f1 /. i as Point of (Euclid 2) by EUCLID:22;
reconsider F2 = { (LSeg (f2,k)) where k is Nat : ( 1 <= k & k + 1 <= len f2 ) } as Subset-Family of (TOP-REAL 2) by Th25;
assume that
A1: f1,f2 are_generators_of P and
A2: 1 < i and
A3: i < len f1 ; :: thesis: f1 /. i is_extremal_in P
set P2 = union F2;
A4: (L~ f1) /\ (L~ f2) = {(f1 /. 1),(f1 /. (len f1))} by A1;
reconsider j = i - 1 as Element of NAT by A2, INT_1:3, XREAL_1:48;
1 + 1 <= i by A2, NAT_1:13;
then A5: (1 + 1) - 1 <= j by XREAL_1:9;
reconsider F = { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 & k <> j & k <> j + 1 ) } as Subset-Family of (TOP-REAL 2) by Lm3;
set P1 = union F;
set Q = (union F) \/ (union F2);
A6: j + 1 = i ;
then LSeg (f1,j) = LSeg ((f1 /. j),(f1 /. i)) by A3, A5, TOPREAL1:def 3;
then A7: f1 /. i in LSeg (f1,j) by RLTOPSP1:68;
A8: P = (L~ f1) \/ (L~ f2) by A1;
A9: f1 is being_S-Seq by A1;
then A10: f1 is one-to-one ;
A11: len f1 >= 1 + 1 by A9;
A12: i + 1 <= len f1 by A3, NAT_1:13;
then A13: LSeg (f1,i) in { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 ) } by A2;
LSeg (f1,i) = LSeg ((f1 /. i),(f1 /. (i + 1))) by A2, A12, TOPREAL1:def 3;
then A14: f1 /. i in LSeg (f1,i) by RLTOPSP1:68;
then A15: f1 /. i in L~ f1 by A13, TARSKI:def 4;
not f1 /. i in (union F) \/ (union F2)

proof

assume A16: f1 /. i in (union F) \/ (union F2) ; :: thesis: contradiction

per cases ( f1 /. i in union F or f1 /. i in union F2 ) by A16, XBOOLE_0:def 3;

suppose A17: f1 /. i in union F ; :: thesis: contradiction

A18: f1 is s.n.c. by A9;
consider Z being set such that
A19: f1 /. i in Z and
A20: Z in F by A17, TARSKI:def 4;
consider k being Nat such that
A21: LSeg (f1,k) = Z and
1 <= k and
k + 1 <= len f1 and
A22: k <> i - 1 and
A23: k <> i by A20;
( k < j + 1 or i < k ) by A23, XXREAL_0:1;
then ( k <= j or i < k ) by NAT_1:13;
then A24: ( k < j or i < k ) by A22, XXREAL_0:1;

now :: thesis: contradiction

per cases ( j - k > 0 or k - i > 0 ) by A24, XREAL_1:50;

suppose j - k > 0 ; :: thesis: contradiction

then 1 + (j - k) > 1 + 0 by XREAL_1:6;
then i - k > 1 ;
then k + 1 < i by XREAL_1:20;
then LSeg (f1,k) misses LSeg (f1,i) by A18;
then (LSeg (f1,k)) /\ (LSeg (f1,i)) = {} by XBOOLE_0:def 7;
hence contradiction by A14, A19, A21, XBOOLE_0:def 4; :: thesis: verum

end;

suppose k - i > 0 ; :: thesis: contradiction

then (k - i) + 1 > 0 + 1 by XREAL_1:6;
then k - j > 1 ;
then j + 1 < k by XREAL_1:20;
then LSeg (f1,j) misses LSeg (f1,k) by A18;
then (LSeg (f1,j)) /\ (LSeg (f1,k)) = {} by XBOOLE_0:def 7;
hence contradiction by A7, A19, A21, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A25: f1 /. i in union F2 ; :: thesis: contradiction

1 <= len f1 by A11, XXREAL_0:2;
then 1 in Seg (len f1) by FINSEQ_1:1;
then A26: 1 in dom f1 by FINSEQ_1:def 3;
1 <= len f1 by A2, A3, XXREAL_0:2;
then A27: len f1 in dom f1 by FINSEQ_3:25;
i in Seg (len f1) by A2, A3, FINSEQ_1:1;
then A28: i in dom f1 by FINSEQ_1:def 3;
f1 /. i in {(f1 /. 1),(f1 /. (len f1))} by A4, A15, A25, XBOOLE_0:def 4;
then ( f1 /. i = f1 /. 1 or f1 /. i = f1 /. (len f1) ) by TARSKI:def 2;
hence contradiction by A2, A3, A10, A26, A28, A27, PARTFUN2:10; :: thesis: verum

end;

end;

end;

then A29: u0 in ((union F) \/ (union F2)) ` by SUBSET_1:29;
A30: f1 is alternating by A1;
A31: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def 8;
then reconsider QQ = ((union F) \/ (union F2)) ` as Subset of (TopSpaceMetr (Euclid 2)) ;
A32: f1 is special by A9;
( union F is closed & union F2 is closed ) by Lm4, Th26;
then (union F) \/ (union F2) is closed by TOPS_1:9;
then ((union F) \/ (union F2)) ` is open by TOPS_1:3;
then QQ is open by A31, PRE_TOPC:30;
then consider r0 being Real such that
A33: r0 > 0 and
A34: Ball (u0,r0) c= ((union F) \/ (union F2)) ` by A29, TOPMETR:15;
reconsider r0 = r0 as Real ;
A35: j + 2 <= len f1 by A12;

now :: thesis: for y being object holds
( ( y in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) implies y in union { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 ) } ) & ( y in union { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 ) } implies y in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) ) )

let y be object ; :: thesis: ( ( y in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) implies y in union { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 ) } ) & ( y in union { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 ) } implies b₁ in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) ) )

hereby :: thesis: ( y in union { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 ) } implies b₁ in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) )

assume y in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) ; :: thesis: y in union { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 ) }
then A36: ( y in (union F) \/ (LSeg (f1,j)) or y in LSeg (f1,i) ) by XBOOLE_0:def 3;

per cases ( y in union F or y in LSeg (f1,j) or y in LSeg (f1,i) ) by A36, XBOOLE_0:def 3;

suppose y in union F ; :: thesis: y in union { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 ) }

then consider Z3 being set such that
A37: y in Z3 and
A38: Z3 in F by TARSKI:def 4;
ex k being Nat st
( LSeg (f1,k) = Z3 & 1 <= k & k + 1 <= len f1 & not k = i - 1 & not k = i ) by A38;
then Z3 in { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 ) } ;
hence y in union { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 ) } by A37, TARSKI:def 4; :: thesis: verum

end;

suppose A39: y in LSeg (f1,j) ; :: thesis: y in union { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 ) }

LSeg (f1,j) in { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 ) } by A3, A6, A5;
hence y in union { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 ) } by A39, TARSKI:def 4; :: thesis: verum

end;

suppose y in LSeg (f1,i) ; :: thesis: y in union { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 ) }

hence y in union { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 ) } by A13, TARSKI:def 4; :: thesis: verum

end;

end;

end;

assume y in union { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 ) } ; :: thesis: b₁ in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i))
then consider Z2 being set such that
A40: y in Z2 and
A41: Z2 in { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 ) } by TARSKI:def 4;
consider k being Nat such that
A42: LSeg (f1,k) = Z2 and
A43: ( 1 <= k & k + 1 <= len f1 ) by A41;

per cases ( k = i - 1 or k = i or ( k <> i - 1 & k <> i ) ) ;

suppose A44: ( k = i - 1 or k = i ) ; :: thesis: b₁ in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i))

now :: thesis: y in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i))

per cases ( k = i - 1 or k = i ) by A44;

suppose k = i - 1 ; :: thesis: y in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i))

then y in (LSeg (f1,j)) \/ (LSeg (f1,i)) by A40, A42, XBOOLE_0:def 3;
then y in (union F) \/ ((LSeg (f1,j)) \/ (LSeg (f1,i))) by XBOOLE_0:def 3;
hence y in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) by XBOOLE_1:4; :: thesis: verum

end;

suppose k = i ; :: thesis: y in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i))

hence y in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) by A40, A42, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence y in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) ; :: thesis: verum

end;

suppose ( k <> i - 1 & k <> i ) ; :: thesis: b₁ in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i))

then Z2 in F by A42, A43;
then y in union F by A40, TARSKI:def 4;
then y in (union F) \/ ((LSeg (f1,j)) \/ (LSeg (f1,i))) by XBOOLE_0:def 3;
hence y in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) by XBOOLE_1:4; :: thesis: verum

end;

end;

end;

then A45: ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) = union { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 ) } by TARSKI:2;

A46: now :: thesis: for p, q being Point of (TOP-REAL 2) st f1 /. i in LSeg (p,q) & LSeg (p,q) c= P & not f1 /. i = p holds
f1 /. i = q

let p, q be Point of (TOP-REAL 2); :: thesis: ( f1 /. i in LSeg (p,q) & LSeg (p,q) c= P & not f1 /. i = b₁ implies f1 /. i = b₂ )
assume that
A47: f1 /. i in LSeg (p,q) and
A48: LSeg (p,q) c= P ; :: thesis: ( f1 /. i = b₁ or f1 /. i = b₂ )

per cases ( LSeg (p,q) c= (LSeg (f1,j)) \/ (LSeg (f1,i)) or not LSeg (p,q) c= (LSeg (f1,j)) \/ (LSeg (f1,i)) ) ;

suppose A49: LSeg (p,q) c= (LSeg (f1,j)) \/ (LSeg (f1,i)) ; :: thesis: ( f1 /. i = b₁ or f1 /. i = b₂ )

f1 /. i is_extremal_in (LSeg (f1,j)) \/ (LSeg (f1,i)) by A30, A6, A5, A35, A32, Th36;
hence ( f1 /. i = p or f1 /. i = q ) by A47, A49; :: thesis: verum

end;

suppose not LSeg (p,q) c= (LSeg (f1,j)) \/ (LSeg (f1,i)) ; :: thesis: ( f1 /. i = b₁ or f1 /. i = b₂ )

then consider x being object such that
A50: x in LSeg (p,q) and
A51: not x in (LSeg (f1,j)) \/ (LSeg (f1,i)) ;
reconsider p8 = x as Point of (TOP-REAL 2) by A50;
A52: LSeg (p,q) = (LSeg (p,p8)) \/ (LSeg (p8,q)) by A50, TOPREAL1:5;

now :: thesis: ( f1 /. i = p or f1 /. i = q )

per cases ( f1 /. i in LSeg (p,p8) or f1 /. i in LSeg (p8,q) ) by A47, A52, XBOOLE_0:def 3;

suppose A53: f1 /. i in LSeg (p,p8) ; :: thesis: ( f1 /. i = p or f1 /. i = q )

now :: thesis: not f1 /. i <> p

assume f1 /. i <> p ; :: thesis: contradiction
then consider q3 being Point of (TOP-REAL 2) such that
A54: not q3 in (LSeg (f1,j)) \/ (LSeg (f1,i)) and
A55: q3 in LSeg (p8,p) and
A56: q3 in Ball (u0,r0) by A30, A5, A35, A32, A33, A34, A51, A53, Th37;
A57: not q3 in (union F) \/ (union F2) by A34, A56, XBOOLE_0:def 5;
then not q3 in union F by XBOOLE_0:def 3;
then not q3 in (union F) \/ ((LSeg (f1,j)) \/ (LSeg (f1,i))) by A54, XBOOLE_0:def 3;
then A58: not q3 in union { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 ) } by A45, XBOOLE_1:4;
LSeg (p8,p) c= LSeg (p,q) by A52, XBOOLE_1:7;
then A59: LSeg (p8,p) c= P by A48;
not q3 in L~ f2 by A57, XBOOLE_0:def 3;
hence contradiction by A8, A55, A58, A59, XBOOLE_0:def 3; :: thesis: verum

end;

hence ( f1 /. i = p or f1 /. i = q ) ; :: thesis: verum

end;

suppose A60: f1 /. i in LSeg (p8,q) ; :: thesis: ( f1 /. i = p or f1 /. i = q )

now :: thesis: not f1 /. i <> q

assume f1 /. i <> q ; :: thesis: contradiction
then consider q3 being Point of (TOP-REAL 2) such that
A61: not q3 in (LSeg (f1,j)) \/ (LSeg (f1,i)) and
A62: q3 in LSeg (p8,q) and
A63: q3 in Ball (u0,r0) by A30, A5, A35, A32, A33, A34, A51, A60, Th37;
A64: not q3 in (union F) \/ (union F2) by A34, A63, XBOOLE_0:def 5;
then not q3 in union F by XBOOLE_0:def 3;
then not q3 in (union F) \/ ((LSeg (f1,j)) \/ (LSeg (f1,i))) by A61, XBOOLE_0:def 3;
then A65: not q3 in union { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 ) } by A45, XBOOLE_1:4;
LSeg (p8,q) c= LSeg (p,q) by A52, XBOOLE_1:7;
then A66: LSeg (p8,q) c= P by A48;
not q3 in L~ f2 by A64, XBOOLE_0:def 3;
hence contradiction by A8, A62, A65, A66, XBOOLE_0:def 3; :: thesis: verum

end;

hence ( f1 /. i = p or f1 /. i = q ) ; :: thesis: verum

end;

end;

end;

hence ( f1 /. i = p or f1 /. i = q ) ; :: thesis: verum

end;

end;

end;

f1 /. i in union { (LSeg (f1,k)) where k is Nat : ( 1 <= k & k + 1 <= len f1 ) } by A14, A13, TARSKI:def 4;
then f1 /. i in P by A8, XBOOLE_0:def 3;
hence f1 /. i is_extremal_in P by A46; :: thesis: verum