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 )
assume that
A1: f1,f2 are_generators_of P and
A2: ( 1 < i & i < len f1 ) ; :: thesis: f1 /. i is_extremal_in P
A3: f1 is alternating by A1, Def5;
A4: f1 is being_S-Seq by A1, Def5;
set p0 = f1 /. i;
A5: ( 1 <= i & i + 1 <= len f1 ) by A2, NAT_1:13;
reconsider j = i - 1 as Element of NAT by A2, INT_1:16, XREAL_1:50;
A6: j + 1 = i ;
1 + 1 <= i by A2, NAT_1:13;
then A7: (1 + 1) - 1 <= j by XREAL_1:11;
then A8: ( 1 <= j & j + 2 <= len f1 ) by A5;
A9: f1 is special by A4, TOPREAL1:def 10;
set q1 = f1 /. 1;
set q2 = f1 /. (len f1);
A10: ( f1 /. 1 <> f1 /. (len f1) & (L~ f1) /\ (L~ f2) = {(f1 /. 1),(f1 /. (len f1))} & P = (L~ f1) \/ (L~ f2) ) by A1, Def5;
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;
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;
set P2 = union F2;
set Q = (union F) \/ (union F2);
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 ) } ;
( union F is closed & union F2 is closed ) by Lm4, Th48;
then (union F) \/ (union F2) is closed by TOPS_1:36;
then A11: ((union F) \/ (union F2)) ` is open by TOPS_1:29;
A12: ( LSeg f1,j = LSeg (f1 /. j),(f1 /. i) & LSeg f1,i = LSeg (f1 /. i),(f1 /. (i + 1)) ) by A2, A5, A6, A7, TOPREAL1:def 5;
A13: ( f1 is one-to-one & len f1 >= 1 + 1 ) by A4, TOPREAL1:def 10;
A14: ( f1 /. i in LSeg f1,j & f1 /. i in LSeg f1,i ) by A12, RLTOPSP1:69;
A15: LSeg f1,i in { (LSeg f1,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } by A5;
then A16: f1 /. i in union { (LSeg f1,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } by A14, TARSKI:def 4;
A17: f1 /. i in L~ f1 by A14, A15, TARSKI:def 4;
A18: ((union F) \/ (LSeg f1,j)) \/ (LSeg f1,i) = union { (LSeg f1,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) }

proof

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 A19: ( 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 A19, 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
A20: y in Z3 and
A21: 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 A21;
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 A20, TARSKI:def 4; :: thesis: verum

end;

suppose A22: 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 A2, A6, A7;
hence y in union { (LSeg f1,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } by A22, 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 A15, 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
A23: y in Z2 and
A24: 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
A25: LSeg f1,k = Z2 and
A26: ( 1 <= k & k + 1 <= len f1 ) by A24;

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

suppose A27: ( 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 A27;

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 A23, A25, 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 A23, A25, 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 A25, A26;
then y in union F by A23, 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;

hence ((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; :: thesis: verum

end;

A28: not f1 /. i in (union F) \/ (union F2)

proof

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

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

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

then consider Z being set such that
A30: ( f1 /. i in Z & Z in F ) by TARSKI:def 4;
consider k being Element of NAT such that
A31: LSeg f1,k = Z and
A32: ( 1 <= k & k + 1 <= len f1 & k <> i - 1 & k <> i ) by A30;
( k < j + 1 or i < k ) by A32, XXREAL_0:1;
then ( k <= j or i < k ) by NAT_1:13;
then A33: ( k < j or i < k ) by A32, XXREAL_0:1;
A34: f1 is s.n.c. by A4, TOPREAL1:def 10;

now

per cases ( j - k > 0 or k - i > 0 ) by A33, 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 A34, TOPREAL1:def 9;
then (LSeg f1,k) /\ (LSeg f1,i) = {} by XBOOLE_0:def 7;
hence contradiction by A14, A30, A31, 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 A34, TOPREAL1:def 9;
then (LSeg f1,j) /\ (LSeg f1,k) = {} by XBOOLE_0:def 7;
hence contradiction by A14, A30, A31, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

then f1 /. i in {(f1 /. 1),(f1 /. (len f1))} by A10, A17, XBOOLE_0:def 4;
then A35: ( f1 /. i = f1 /. 1 or f1 /. i = f1 /. (len f1) ) by TARSKI:def 2;
1 <= len f1 by A13, XXREAL_0:2;
then 1 in Seg (len f1) by FINSEQ_1:3;
then A36: 1 in dom f1 by FINSEQ_1:def 3;
i in Seg (len f1) by A2, FINSEQ_1:3;
then A37: i in dom f1 by FINSEQ_1:def 3;
1 <= len f1 by A2, XXREAL_0:2;
then len f1 in dom f1 by FINSEQ_3:27;
hence contradiction by A2, A13, A35, A36, A37, PARTFUN2:17; :: thesis: verum

end;

end;

end;

reconsider u0 = f1 /. i as Point of (Euclid 2) by EUCLID:25;
X: 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)) ;
Y: QQ is open by X, A11, PRE_TOPC:60;
u0 in ((union F) \/ (union F2)) ` by A28, SUBSET_1:50;
then consider r0 being real number such that
A38: ( r0 > 0 & Ball u0,r0 c= ((union F) \/ (union F2)) ` ) by Y, TOPMETR:22;
reconsider r0 = r0 as Real by XREAL_0:def 1;

A39: 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 A40: ( f1 /. i in LSeg p,q & 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 A41: 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 A3, A6, A8, A9, Th59;
hence ( f1 /. i = p or f1 /. i = q ) by A40, A41, 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
A42: ( x in LSeg p,q & not x in (LSeg f1,j) \/ (LSeg f1,i) ) by TARSKI:def 3;
reconsider p8 = x as Point of (TOP-REAL 2) by A42;
A43: LSeg p,q = (LSeg p,p8) \/ (LSeg p8,q) by A42, TOPREAL1:11;

now

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

suppose A44: 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
A45: ( not q3 in (LSeg f1,j) \/ (LSeg f1,i) & q3 in LSeg p8,p & q3 in Ball u0,r0 ) by A3, A8, A9, A38, A42, A44, Th60;
A46: not q3 in (union F) \/ (union F2) by A38, A45, XBOOLE_0:def 5;
then ( not q3 in union F & not q3 in union F2 ) by XBOOLE_0:def 3;
then not q3 in (union F) \/ ((LSeg f1,j) \/ (LSeg f1,i)) by A45, XBOOLE_0:def 3;
then A47: not q3 in union { (LSeg f1,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } by A18, XBOOLE_1:4;
A48: not q3 in L~ f2 by A46, XBOOLE_0:def 3;
LSeg p8,p c= LSeg p,q by A43, XBOOLE_1:7;
then LSeg p8,p c= P by A40, XBOOLE_1:1;
hence contradiction by A10, A45, A47, A48, XBOOLE_0:def 3; :: thesis: verum

end;

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

end;

suppose A49: 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
A50: ( not q3 in (LSeg f1,j) \/ (LSeg f1,i) & q3 in LSeg p8,q & q3 in Ball u0,r0 ) by A3, A8, A9, A38, A42, A49, Th60;
A51: not q3 in (union F) \/ (union F2) by A38, A50, XBOOLE_0:def 5;
then ( not q3 in union F & not q3 in union F2 ) by XBOOLE_0:def 3;
then not q3 in (union F) \/ ((LSeg f1,j) \/ (LSeg f1,i)) by A50, XBOOLE_0:def 3;
then A52: not q3 in union { (LSeg f1,k) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } by A18, XBOOLE_1:4;
A53: not q3 in L~ f2 by A51, XBOOLE_0:def 3;
LSeg p8,q c= LSeg p,q by A43, XBOOLE_1:7;
then LSeg p8,q c= P by A40, XBOOLE_1:1;
hence contradiction by A10, A50, A52, A53, 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 P by A10, A16, XBOOLE_0:def 3;
hence f1 /. i is_extremal_in P by A39, Def1; :: thesis: verum