set p0 = |[0 ,0 ]|;
set p01 = |[0 ,1]|;
set p10 = |[1,0 ]|;
set p1 = |[1,1]|;
set L4 = { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } ;
set L3 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } ;
set L2 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } ;
set L1 = { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } ;
A1: |[1,1]| `1 = 1 by EUCLID:56;
reconsider f2 = <*|[0 ,0 ]|,|[1,0 ]|,|[1,1]|*> as FinSequence of (TOP-REAL 2) ;
reconsider f1 = <*|[0 ,0 ]|,|[0 ,1]|,|[1,1]|*> as FinSequence of (TOP-REAL 2) ;
A2: |[0 ,0 ]| `1 = 0 by EUCLID:56;
take f1 ; :: thesis: ex f2 being FinSequence of (TOP-REAL 2) st
( f1 is being_S-Seq & f2 is being_S-Seq & R^2-unit_square = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {|[0 ,0 ]|,|[1,1]|} & f1 /. 1 = |[0 ,0 ]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0 ,0 ]| & f2 /. (len f2) = |[1,1]| )
take f2 ; :: thesis: ( f1 is being_S-Seq & f2 is being_S-Seq & R^2-unit_square = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {|[0 ,0 ]|,|[1,1]|} & f1 /. 1 = |[0 ,0 ]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0 ,0 ]| & f2 /. (len f2) = |[1,1]| )
A3: f1 /. 2 = |[0 ,1]| by FINSEQ_4:27;

now

assume { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } meets { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } ; :: thesis: contradiction
then consider x being set such that
A4: x in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } and
A5: x in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } by XBOOLE_0:3;
A6: ex p2 being Point of (TOP-REAL 2) st
( p2 = x & p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 0 ) by A5;
ex p being Point of (TOP-REAL 2) st
( p = x & p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) by A4;
hence contradiction by A6; :: thesis: verum

end;

then A7: { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } = {} by XBOOLE_0:def 7;
A8: |[1,0 ]| `2 = 0 by EUCLID:56;
A9: |[1,0 ]| `1 = 1 by EUCLID:56;
A10: len f2 = 1 + 2 by FINSEQ_1:62;
then A11: 1 + 1 <= len f2 ;
A12: f1 /. 3 = |[1,1]| by FINSEQ_4:27;
A13: f1 /. 1 = |[0 ,0 ]| by FINSEQ_4:27;
A14: { (LSeg f1,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } c= {(LSeg |[0 ,0 ]|,|[0 ,1]|),(LSeg |[0 ,1]|,|[1,1]|)}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (LSeg f1,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } or a in {(LSeg |[0 ,0 ]|,|[0 ,1]|),(LSeg |[0 ,1]|,|[1,1]|)} )
assume a in { (LSeg f1,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } ; :: thesis: a in {(LSeg |[0 ,0 ]|,|[0 ,1]|),(LSeg |[0 ,1]|,|[1,1]|)}
then consider i being Element of NAT such that
A15: a = LSeg f1,i and
A16: 1 <= i and
A17: i + 1 <= len f1 ;
i + 1 <= 2 + 1 by A17, FINSEQ_1:62;
then i <= 1 + 1 by XREAL_1:8;
then ( i = 1 or i = 2 ) by A16, NAT_1:9;
then ( a = LSeg |[0 ,0 ]|,|[0 ,1]| or a = LSeg |[0 ,1]|,|[1,1]| ) by A13, A3, A12, A15, A17, Def5;
hence a in {(LSeg |[0 ,0 ]|,|[0 ,1]|),(LSeg |[0 ,1]|,|[1,1]|)} by TARSKI:def 2; :: thesis: verum

end;

A18: len f1 = 1 + 2 by FINSEQ_1:62;
then A19: 1 + 1 <= len f1 ;
1 + 1 in Seg (len f1) by A18, FINSEQ_1:3;
then LSeg |[0 ,0 ]|,|[0 ,1]| = LSeg f1,1 by A18, A13, A3, Def5;
then A20: LSeg |[0 ,0 ]|,|[0 ,1]| in { (LSeg f1,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } by A19;
A21: f2 /. 3 = |[1,1]| by FINSEQ_4:27;
A22: |[0 ,0 ]| `2 = 0 by EUCLID:56;
thus f1 is being_S-Seq :: thesis: ( f2 is being_S-Seq & R^2-unit_square = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {|[0 ,0 ]|,|[1,1]|} & f1 /. 1 = |[0 ,0 ]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0 ,0 ]| & f2 /. (len f2) = |[1,1]| )

proof

A23: |[0 ,1]| <> |[1,1]| by A1, EUCLID:56;
|[0 ,0 ]| <> |[0 ,1]| by A22, EUCLID:56;
hence f1 is one-to-one by A1, A2, A23, FINSEQ_3:104; :: according to TOPREAL1:def 10 :: thesis: ( len f1 >= 2 & f1 is unfolded & f1 is s.n.c. & f1 is special )
thus len f1 >= 2 by A18; :: thesis: ( f1 is unfolded & f1 is s.n.c. & f1 is special )
thus f1 is unfolded :: thesis: ( f1 is s.n.c. & f1 is special )

proof

A24: for x being set holds
( x in (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) iff x = |[0 ,1]| )

proof

let x be set ; :: thesis: ( x in (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) iff x = |[0 ,1]| )
thus ( x in (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) implies x = |[0 ,1]| ) :: thesis: ( x = |[0 ,1]| implies x in (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) )

proof

assume A25: x in (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) ; :: thesis: x = |[0 ,1]|
then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 1 ) } by Th19, XBOOLE_0:def 4;
then A26: ex p2 being Point of (TOP-REAL 2) st
( p2 = x & p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 1 ) ;
x in { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } by A25, Th19, XBOOLE_0:def 4;
then ex p being Point of (TOP-REAL 2) st
( p = x & p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) ;
hence x = |[0 ,1]| by A26, EUCLID:57; :: thesis: verum

end;

assume A27: x = |[0 ,1]| ; :: thesis: x in (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|)
then A28: x in LSeg |[0 ,1]|,|[1,1]| by RLTOPSP1:69;
x in LSeg |[0 ,0 ]|,|[0 ,1]| by A27, RLTOPSP1:69;
hence x in (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A28, XBOOLE_0:def 4; :: thesis: verum

end;

let i be Nat; :: according to TOPREAL1:def 8 :: thesis: ( 1 <= i & i + 2 <= len f1 implies (LSeg f1,i) /\ (LSeg f1,(i + 1)) = {(f1 /. (i + 1))} )
assume that
A29: 1 <= i and
A30: i + 2 <= len f1 ; :: thesis: (LSeg f1,i) /\ (LSeg f1,(i + 1)) = {(f1 /. (i + 1))}
i <= 1 by A18, A30, XREAL_1:8;
then A31: i = 1 by A29, XXREAL_0:1;
1 + 1 in Seg (len f1) by A18, FINSEQ_1:3;
then A32: LSeg f1,1 = LSeg |[0 ,0 ]|,|[0 ,1]| by A18, A13, A3, Def5;
LSeg f1,(1 + 1) = LSeg |[0 ,1]|,|[1,1]| by A18, A3, A12, Def5;
hence (LSeg f1,i) /\ (LSeg f1,(i + 1)) = {(f1 /. (i + 1))} by A3, A31, A32, A24, TARSKI:def 1; :: thesis: verum

end;

thus f1 is s.n.c. :: thesis: f1 is special

proof

let i be Nat; :: according to TOPREAL1:def 9 :: thesis: for j being Nat st i + 1 < j holds
LSeg f1,i misses LSeg f1,j
let j be Nat; :: thesis: ( i + 1 < j implies LSeg f1,i misses LSeg f1,j )
assume A33: i + 1 < j ; :: thesis: LSeg f1,i misses LSeg f1,j

now

per cases ( 1 <= i or not 1 <= i or not i + 1 <= len f1 ) ;

suppose 1 <= i ; :: thesis: (LSeg f1,i) /\ (LSeg f1,j) = {}

then A34: 1 + 1 <= i + 1 by XREAL_1:8;

now

per cases ( ( 1 <= j & j + 1 <= len f1 ) or not 1 <= j or not j + 1 <= len f1 ) ;

case ( 1 <= j & j + 1 <= len f1 ) ; :: thesis: contradiction

then j <= 2 by A18, XREAL_1:8;
hence contradiction by A33, A34, XXREAL_0:2; :: thesis: verum

end;

case ( not 1 <= j or not j + 1 <= len f1 ) ; :: thesis: (LSeg f1,i) /\ (LSeg f1,j) = {}

then LSeg f1,j = {} by Def5;
hence (LSeg f1,i) /\ (LSeg f1,j) = {} ; :: thesis: verum

end;

end;

end;

hence (LSeg f1,i) /\ (LSeg f1,j) = {} ; :: thesis: verum

end;

suppose ( not 1 <= i or not i + 1 <= len f1 ) ; :: thesis: (LSeg f1,i) /\ (LSeg f1,j) = {}

then LSeg f1,i = {} by Def5;
hence (LSeg f1,i) /\ (LSeg f1,j) = {} ; :: thesis: verum

end;

end;

end;

hence (LSeg f1,i) /\ (LSeg f1,j) = {} ; :: according to XBOOLE_0:def 7 :: thesis: verum

end;

let i be Nat; :: according to TOPREAL1:def 7 :: thesis: ( 1 <= i & i + 1 <= len f1 & not (f1 /. i) `1 = (f1 /. (i + 1)) `1 implies (f1 /. i) `2 = (f1 /. (i + 1)) `2 )
assume that
A35: 1 <= i and
A36: i + 1 <= len f1 ; :: thesis: ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 )
A37: i <= 1 + 1 by A18, A36, XREAL_1:8;

per cases ( i = 1 or i = 2 ) by A35, A37, NAT_1:9;

suppose A38: i = 1 ; :: thesis: ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 )

then (f1 /. i) `1 = |[0 ,0 ]| `1 by FINSEQ_4:27
.= 0 by EUCLID:56
.= (f1 /. (i + 1)) `1 by A3, A38, EUCLID:56 ;
hence ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 ) ; :: thesis: verum

end;

suppose A39: i = 2 ; :: thesis: ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 )

then (f1 /. i) `2 = |[0 ,1]| `2 by FINSEQ_4:27
.= 1 by EUCLID:56
.= (f1 /. (i + 1)) `2 by A12, A39, EUCLID:56 ;
hence ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 ) ; :: thesis: verum

end;

end;

end;

A40: f2 /. 2 = |[1,0 ]| by FINSEQ_4:27;
A41: f2 /. 1 = |[0 ,0 ]| by FINSEQ_4:27;
A42: { (LSeg f2,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } c= {(LSeg |[0 ,0 ]|,|[1,0 ]|),(LSeg |[1,0 ]|,|[1,1]|)}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (LSeg f2,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } or a in {(LSeg |[0 ,0 ]|,|[1,0 ]|),(LSeg |[1,0 ]|,|[1,1]|)} )
assume a in { (LSeg f2,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } ; :: thesis: a in {(LSeg |[0 ,0 ]|,|[1,0 ]|),(LSeg |[1,0 ]|,|[1,1]|)}
then consider i being Element of NAT such that
A43: a = LSeg f2,i and
A44: 1 <= i and
A45: i + 1 <= len f2 ;
i + 1 <= 2 + 1 by A45, FINSEQ_1:62;
then i <= 1 + 1 by XREAL_1:8;
then ( i = 1 or i = 2 ) by A44, NAT_1:9;
then ( a = LSeg |[0 ,0 ]|,|[1,0 ]| or a = LSeg |[1,0 ]|,|[1,1]| ) by A41, A40, A21, A43, A45, Def5;
hence a in {(LSeg |[0 ,0 ]|,|[1,0 ]|),(LSeg |[1,0 ]|,|[1,1]|)} by TARSKI:def 2; :: thesis: verum

end;

1 + 1 in Seg (len f2) by A10, FINSEQ_1:3;
then LSeg |[0 ,0 ]|,|[1,0 ]| = LSeg f2,1 by A10, A41, A40, Def5;
then A46: LSeg |[0 ,0 ]|,|[1,0 ]| in { (LSeg f2,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } by A11;
LSeg |[1,0 ]|,|[1,1]| = LSeg f2,2 by A10, A40, A21, Def5;
then LSeg |[1,0 ]|,|[1,1]| in { (LSeg f2,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } by A10;
then {(LSeg |[0 ,0 ]|,|[1,0 ]|),(LSeg |[1,0 ]|,|[1,1]|)} c= { (LSeg f2,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } by A46, ZFMISC_1:38;
then A47: L~ f2 = union {(LSeg |[0 ,0 ]|,|[1,0 ]|),(LSeg |[1,0 ]|,|[1,1]|)} by A42, XBOOLE_0:def 10;
A48: |[1,1]| `2 = 1 by EUCLID:56;
thus f2 is being_S-Seq :: thesis: ( R^2-unit_square = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {|[0 ,0 ]|,|[1,1]|} & f1 /. 1 = |[0 ,0 ]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0 ,0 ]| & f2 /. (len f2) = |[1,1]| )

proof

thus f2 is one-to-one by A1, A48, A9, A8, A2, FINSEQ_3:104; :: according to TOPREAL1:def 10 :: thesis: ( len f2 >= 2 & f2 is unfolded & f2 is s.n.c. & f2 is special )
thus len f2 >= 2 by A10; :: thesis: ( f2 is unfolded & f2 is s.n.c. & f2 is special )
thus f2 is unfolded :: thesis: ( f2 is s.n.c. & f2 is special )

proof

A49: for x being set holds
( x in (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) iff x = |[1,0 ]| )

proof

let x be set ; :: thesis: ( x in (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) iff x = |[1,0 ]| )
thus ( x in (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) implies x = |[1,0 ]| ) :: thesis: ( x = |[1,0 ]| implies x in (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) )

proof

assume A50: x in (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) ; :: thesis: x = |[1,0 ]|
then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = 1 & p2 `2 <= 1 & p2 `2 >= 0 ) } by Th19, XBOOLE_0:def 4;
then A51: ex p2 being Point of (TOP-REAL 2) st
( p2 = x & p2 `1 = 1 & p2 `2 <= 1 & p2 `2 >= 0 ) ;
x in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } by A50, Th19, XBOOLE_0:def 4;
then ex p being Point of (TOP-REAL 2) st
( p = x & p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) ;
hence x = |[1,0 ]| by A51, EUCLID:57; :: thesis: verum

end;

assume A52: x = |[1,0 ]| ; :: thesis: x in (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|)
then A53: x in LSeg |[1,0 ]|,|[1,1]| by RLTOPSP1:69;
x in LSeg |[0 ,0 ]|,|[1,0 ]| by A52, RLTOPSP1:69;
hence x in (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) by A53, XBOOLE_0:def 4; :: thesis: verum

end;

let i be Nat; :: according to TOPREAL1:def 8 :: thesis: ( 1 <= i & i + 2 <= len f2 implies (LSeg f2,i) /\ (LSeg f2,(i + 1)) = {(f2 /. (i + 1))} )
assume that
A54: 1 <= i and
A55: i + 2 <= len f2 ; :: thesis: (LSeg f2,i) /\ (LSeg f2,(i + 1)) = {(f2 /. (i + 1))}
i <= 1 by A10, A55, XREAL_1:8;
then A56: i = 1 by A54, XXREAL_0:1;
1 + 1 in Seg (len f2) by A10, FINSEQ_1:3;
then A57: LSeg f2,1 = LSeg |[0 ,0 ]|,|[1,0 ]| by A10, A41, A40, Def5;
LSeg f2,(1 + 1) = LSeg |[1,0 ]|,|[1,1]| by A10, A40, A21, Def5;
hence (LSeg f2,i) /\ (LSeg f2,(i + 1)) = {(f2 /. (i + 1))} by A40, A56, A57, A49, TARSKI:def 1; :: thesis: verum

end;

thus f2 is s.n.c. :: thesis: f2 is special

proof

let i be Nat; :: according to TOPREAL1:def 9 :: thesis: for j being Nat st i + 1 < j holds
LSeg f2,i misses LSeg f2,j
let j be Nat; :: thesis: ( i + 1 < j implies LSeg f2,i misses LSeg f2,j )
assume A58: i + 1 < j ; :: thesis: LSeg f2,i misses LSeg f2,j

per cases ( 1 <= i or not 1 <= i or not i + 1 <= len f2 ) ;

suppose 1 <= i ; :: thesis: LSeg f2,i misses LSeg f2,j

then A59: 1 + 1 <= i + 1 by XREAL_1:8;

now

per cases ( ( 1 <= j & j + 1 <= len f2 ) or not 1 <= j or not j + 1 <= len f2 ) ;

case ( 1 <= j & j + 1 <= len f2 ) ; :: thesis: contradiction

then j <= 2 by A10, XREAL_1:8;
hence contradiction by A58, A59, XXREAL_0:2; :: thesis: verum

end;

case ( not 1 <= j or not j + 1 <= len f2 ) ; :: thesis: (LSeg f2,i) /\ (LSeg f2,j) = {}

then LSeg f2,j = {} by Def5;
hence (LSeg f2,i) /\ (LSeg f2,j) = {} ; :: thesis: verum

end;

end;

end;

hence (LSeg f2,i) /\ (LSeg f2,j) = {} ; :: according to XBOOLE_0:def 7 :: thesis: verum

end;

suppose ( not 1 <= i or not i + 1 <= len f2 ) ; :: thesis: LSeg f2,i misses LSeg f2,j

then LSeg f2,i = {} by Def5;
hence (LSeg f2,i) /\ (LSeg f2,j) = {} ; :: according to XBOOLE_0:def 7 :: thesis: verum

end;

end;

end;

let i be Nat; :: according to TOPREAL1:def 7 :: thesis: ( 1 <= i & i + 1 <= len f2 & not (f2 /. i) `1 = (f2 /. (i + 1)) `1 implies (f2 /. i) `2 = (f2 /. (i + 1)) `2 )
assume that
A60: 1 <= i and
A61: i + 1 <= len f2 ; :: thesis: ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 )
A62: i <= 1 + 1 by A10, A61, XREAL_1:8;

per cases ( i = 1 or i = 2 ) by A60, A62, NAT_1:9;

suppose A63: i = 1 ; :: thesis: ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 )

then (f2 /. i) `2 = |[0 ,0 ]| `2 by FINSEQ_4:27
.= 0 by EUCLID:56
.= (f2 /. (i + 1)) `2 by A40, A63, EUCLID:56 ;
hence ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 ) ; :: thesis: verum

end;

suppose A64: i = 2 ; :: thesis: ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 )

then (f2 /. i) `1 = |[1,0 ]| `1 by FINSEQ_4:27
.= 1 by EUCLID:56
.= (f2 /. (i + 1)) `1 by A21, A64, EUCLID:56 ;
hence ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 ) ; :: thesis: verum

end;

end;

end;

A65: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by Th26, XBOOLE_0:def 7;
LSeg |[0 ,1]|,|[1,1]| = LSeg f1,2 by A18, A3, A12, Def5;
then LSeg |[0 ,1]|,|[1,1]| in { (LSeg f1,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } by A18;
then {(LSeg |[0 ,0 ]|,|[0 ,1]|),(LSeg |[0 ,1]|,|[1,1]|)} c= { (LSeg f1,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } by A20, ZFMISC_1:38;
then A66: L~ f1 = union {(LSeg |[0 ,0 ]|,|[0 ,1]|),(LSeg |[0 ,1]|,|[1,1]|)} by A14, XBOOLE_0:def 10;
then L~ f1 = (LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|) by ZFMISC_1:93;
hence R^2-unit_square = (L~ f1) \/ (L~ f2) by A47, ZFMISC_1:93; :: thesis: ( (L~ f1) /\ (L~ f2) = {|[0 ,0 ]|,|[1,1]|} & f1 /. 1 = |[0 ,0 ]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0 ,0 ]| & f2 /. (len f2) = |[1,1]| )
L~ f2 = (LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|) by A47, ZFMISC_1:93;
hence (L~ f1) /\ (L~ f2) = ({ p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } ) /\ ({ p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } ) by A66, Th19, ZFMISC_1:93
.= (({ p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } ) /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } ) \/ (({ p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } ) /\ { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } ) by XBOOLE_1:23
.= (({ p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } ) \/ ({ p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } )) \/ (({ p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } ) /\ { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } ) by XBOOLE_1:23
.= (({ p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } ) \/ ({ p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } )) \/ (({ p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } ) \/ ({ p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } /\ { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } )) by XBOOLE_1:23
.= {|[0 ,0 ]|,|[1,1]|} by A7, A65, Th19, Th23, Th24, ENUMSET1:41 ;
:: thesis: ( f1 /. 1 = |[0 ,0 ]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0 ,0 ]| & f2 /. (len f2) = |[1,1]| )
thus ( f1 /. 1 = |[0 ,0 ]| & f1 /. (len f1) = |[1,1]| & f2 /. 1 = |[0 ,0 ]| & f2 /. (len f2) = |[1,1]| ) by A18, A10, FINSEQ_4:27; :: thesis: verum