let i be Element of 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 Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } ;
set PP = union { (LSeg f1,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } ;
reconsider u0 = f1 /. i as Point of (Euclid 2) by EUCLID:25;
reconsider F2 = { (LSeg f2,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f2 ) } as Subset-Family of (TOP-REAL 2) by Th47;
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, Def5;
reconsider j = i - 1 as Element of NAT by A2, INT_1:16, XREAL_1:50;
1 + 1 <= i by A2, NAT_1:13;
then A5: (1 + 1) - 1 <= j by XREAL_1:11;
reconsider F = { (LSeg f1,k) where k is Element of 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 5;
then A7: f1 /. i in LSeg f1,j by RLTOPSP1:69;
A8: P = (L~ f1) \/ (L~ f2) by A1, Def5;
A9: f1 is being_S-Seq by A1, Def5;
then A10: f1 is one-to-one by TOPREAL1:def 10;
A11: len f1 >= 1 + 1 by A9, TOPREAL1:def 10;
A12: i + 1 <= len f1 by A3, NAT_1:13;
then A13: LSeg f1,i in { (LSeg f1,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } by A2;
LSeg f1,i = LSeg (f1 /. i),(f1 /. (i + 1)) by A2, A12, TOPREAL1:def 5;
then A14: f1 /. i in LSeg f1,i by RLTOPSP1:69;
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, TOPREAL1:def 10;
consider Z being set such that
A19: f1 /. i in Z and
A20: Z in F by A17, TARSKI:def 4;
consider k being Element of 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

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

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

then 1 + (j - k) > 1 + 0 by XREAL_1:8;
then i - k > 1 ;
then k + 1 < i by XREAL_1:22;
then LSeg f1,k misses LSeg f1,i by A18, TOPREAL1:def 9;
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:8;
then k - j > 1 ;
then j + 1 < k by XREAL_1:22;
then LSeg f1,j misses LSeg f1,k by A18, TOPREAL1:def 9;
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:3;
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:27;
i in Seg (len f1) by A2, A3, FINSEQ_1:3;
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:17; :: thesis: verum

end;

end;

end;

then A29: u0 in ((union F) \/ (union F2)) ` by SUBSET_1:50;
A30: f1 is alternating by A1, Def5;
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, TOPREAL1:def 10;
( union F is closed & union F2 is closed ) by Lm4, Th48;
then (union F) \/ (union F2) is closed by TOPS_1:36;
then ((union F) \/ (union F2)) ` is open by TOPS_1:29;
then QQ is open by A31, PRE_TOPC:60;
then consider r0 being real number such that
A33: r0 > 0 and
A34: Ball u0,r0 c= ((union F) \/ (union F2)) ` by A29, TOPMETR:22;
reconsider r0 = r0 as Real by XREAL_0:def 1;
A35: j + 2 <= len f1 by A12;

now

let y be set ; :: thesis: ( ( y in ((union F) \/ (LSeg f1,j)) \/ (LSeg f1,i) implies y in union { (LSeg f1,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } ) & ( y in union { (LSeg f1,k) where k is Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } ;
hence y in union { (LSeg f1,k) where k is Element of 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 Element of NAT : ( 1 <= k & k + 1 <= len f1 ) }

LSeg f1,j in { (LSeg f1,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } by A3, A6, A5;
hence y in union { (LSeg f1,k) where k is Element of 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 Element of NAT : ( 1 <= k & k + 1 <= len f1 ) }

hence y in union { (LSeg f1,k) where k is Element of 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 Element of 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 Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } by TARSKI:def 4;
consider k being Element of 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

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 Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } by TARSKI:2;

A46: now

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, Th59;
hence ( f1 /. i = p or f1 /. i = q ) by A47, A49, Def1; :: 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 set such that
A50: x in LSeg p,q and
A51: not x in (LSeg f1,j) \/ (LSeg f1,i) by TARSKI:def 3;
reconsider p8 = x as Point of (TOP-REAL 2) by A50;
A52: LSeg p,q = (LSeg p,p8) \/ (LSeg p8,q) by A50, TOPREAL1:11;

now

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

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, Th60;
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 Element of 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, XBOOLE_1:1;
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

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, Th60;
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 Element of 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, XBOOLE_1:1;
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 Element of 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, Def1; :: thesis: verum