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:52;
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:52;
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:18;
now :: thesis: not { 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 ) }
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 object 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 ) } = {} ;
A8: |[1,0]| `2 = 0 by EUCLID:52;
A9: |[1,0]| `1 = 1 by EUCLID:52;
A10: len f2 = 1 + 2 by FINSEQ_1:45;
then A11: 1 + 1 <= len f2 ;
A12: f1 /. 3 = |[1,1]| by FINSEQ_4:18;
A13: f1 /. 1 = |[0,0]| by FINSEQ_4:18;
A14: { (LSeg (f1,i)) where i is Nat : ( 1 <= i & i + 1 <= len f1 ) } c= {(LSeg (|[0,0]|,|[0,1]|)),(LSeg (|[0,1]|,|[1,1]|))}
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (LSeg (f1,i)) where i is 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 Nat : ( 1 <= i & i + 1 <= len f1 ) } ; :: thesis: a in {(LSeg (|[0,0]|,|[0,1]|)),(LSeg (|[0,1]|,|[1,1]|))}
then consider i being 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:45;
then i <= 1 + 1 by XREAL_1:6;
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, Def3;
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:45;
then A19: 1 + 1 <= len f1 ;
1 + 1 in Seg (len f1) by A18, FINSEQ_1:1;
then LSeg (|[0,0]|,|[0,1]|) = LSeg (f1,1) by A18, A13, A3, Def3;
then A20: LSeg (|[0,0]|,|[0,1]|) in { (LSeg (f1,i)) where i is Nat : ( 1 <= i & i + 1 <= len f1 ) } by A19;
A21: f2 /. 3 = |[1,1]| by FINSEQ_4:18;
A22: |[0,0]| `2 = 0 by EUCLID:52;
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:52;
|[0,0]| <> |[0,1]| by A22, EUCLID:52;
hence f1 is one-to-one by A1, A2, A23, FINSEQ_3:95; :: according to TOPREAL1:def 8 :: 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 object holds
( x in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) iff x = |[0,1]| )
proof
let x be object ; :: 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 Th13, 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, Th13, 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:53; :: 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:68;
x in LSeg (|[0,0]|,|[0,1]|) by A27, RLTOPSP1:68;
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 6 :: 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:6;
then A31: i = 1 by A29, XXREAL_0:1;
1 + 1 in Seg (len f1) by A18, FINSEQ_1:1;
then A32: LSeg (f1,1) = LSeg (|[0,0]|,|[0,1]|) by A18, A13, A3, Def3;
LSeg (f1,(1 + 1)) = LSeg (|[0,1]|,|[1,1]|) by A18, A3, A12, Def3;
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 7 :: 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 :: thesis: (LSeg (f1,i)) /\ (LSeg (f1,j)) = {}
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:6;
now :: thesis: ( ( 1 <= j & j + 1 <= len f1 & contradiction ) or ( ( not 1 <= j or not j + 1 <= len f1 ) & (LSeg (f1,i)) /\ (LSeg (f1,j)) = {} ) )
per cases ( ( 1 <= j & j + 1 <= len f1 ) or not 1 <= j or not j + 1 <= len f1 ) ;
case ( not 1 <= j or not j + 1 <= len f1 ) ; :: thesis: (LSeg (f1,i)) /\ (LSeg (f1,j)) = {}
then LSeg (f1,j) = {} by Def3;
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 Def3;
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 5 :: 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:6;
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:18
.= 0 by EUCLID:52
.= (f1 /. (i + 1)) `1 by A3, A38, EUCLID:52 ;
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:18
.= 1 by EUCLID:52
.= (f1 /. (i + 1)) `2 by A12, A39, EUCLID:52 ;
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:18;
A41: f2 /. 1 = |[0,0]| by FINSEQ_4:18;
A42: { (LSeg (f2,i)) where i is Nat : ( 1 <= i & i + 1 <= len f2 ) } c= {(LSeg (|[0,0]|,|[1,0]|)),(LSeg (|[1,0]|,|[1,1]|))}
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (LSeg (f2,i)) where i is 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 Nat : ( 1 <= i & i + 1 <= len f2 ) } ; :: thesis: a in {(LSeg (|[0,0]|,|[1,0]|)),(LSeg (|[1,0]|,|[1,1]|))}
then consider i being 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:45;
then i <= 1 + 1 by XREAL_1:6;
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, Def3;
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:1;
then LSeg (|[0,0]|,|[1,0]|) = LSeg (f2,1) by A10, A41, A40, Def3;
then A46: LSeg (|[0,0]|,|[1,0]|) in { (LSeg (f2,i)) where i is Nat : ( 1 <= i & i + 1 <= len f2 ) } by A11;
LSeg (|[1,0]|,|[1,1]|) = LSeg (f2,2) by A10, A40, A21, Def3;
then LSeg (|[1,0]|,|[1,1]|) in { (LSeg (f2,i)) where i is 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 Nat : ( 1 <= i & i + 1 <= len f2 ) } by A46, ZFMISC_1:32;
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:52;
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:95; :: according to TOPREAL1:def 8 :: 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 object holds
( x in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) iff x = |[1,0]| )
proof
let x be object ; :: 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 Th13, 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, Th13, 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:53; :: 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:68;
x in LSeg (|[0,0]|,|[1,0]|) by A52, RLTOPSP1:68;
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 6 :: 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:6;
then A56: i = 1 by A54, XXREAL_0:1;
1 + 1 in Seg (len f2) by A10, FINSEQ_1:1;
then A57: LSeg (f2,1) = LSeg (|[0,0]|,|[1,0]|) by A10, A41, A40, Def3;
LSeg (f2,(1 + 1)) = LSeg (|[1,0]|,|[1,1]|) by A10, A40, A21, Def3;
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 7 :: 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:6;
now :: thesis: ( ( 1 <= j & j + 1 <= len f2 & contradiction ) or ( ( not 1 <= j or not j + 1 <= len f2 ) & (LSeg (f2,i)) /\ (LSeg (f2,j)) = {} ) )
per cases ( ( 1 <= j & j + 1 <= len f2 ) or not 1 <= j or not j + 1 <= len f2 ) ;
case ( not 1 <= j or not j + 1 <= len f2 ) ; :: thesis: (LSeg (f2,i)) /\ (LSeg (f2,j)) = {}
then LSeg (f2,j) = {} by Def3;
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 Def3;
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 5 :: 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:6;
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:18
.= 0 by EUCLID:52
.= (f2 /. (i + 1)) `2 by A40, A63, EUCLID:52 ;
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:18
.= 1 by EUCLID:52
.= (f2 /. (i + 1)) `1 by A21, A64, EUCLID:52 ;
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 Th20;
LSeg (|[0,1]|,|[1,1]|) = LSeg (f1,2) by A18, A3, A12, Def3;
then LSeg (|[0,1]|,|[1,1]|) in { (LSeg (f1,i)) where i is 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 Nat : ( 1 <= i & i + 1 <= len f1 ) } by A20, ZFMISC_1:32;
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:75;
hence R^2-unit_square = (L~ f1) \/ (L~ f2) by A47, ZFMISC_1:75; :: 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:75;
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, Th13, ZFMISC_1:75
.= (( { 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, Th13, Th17, Th18, ENUMSET1:1 ;
:: 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:18; :: thesis: verum