set L1 = { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } ;
set L2 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } ;
set L3 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } ;
set L4 = { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } ;
set p0 = |[0 ,0 ]|;
set p01 = |[0 ,1]|;
set p10 = |[1,0 ]|;
set p1 = |[1,1]|;
A1: ( |[1,1]| `1 = 1 & |[1,1]| `2 = 1 ) by EUCLID:56;
A2: ( |[1,0 ]| `1 = 1 & |[1,0 ]| `2 = 0 ) by EUCLID:56;
A3: ( |[0 ,0 ]| `1 = 0 & |[0 ,0 ]| `2 = 0 ) by EUCLID:56;
reconsider f1 = <*|[0 ,0 ]|,|[0 ,1]|,|[1,1]|*> as FinSequence of (TOP-REAL 2) ;
reconsider f2 = <*|[0 ,0 ]|,|[1,0 ]|,|[1,1]|*> as FinSequence of (TOP-REAL 2) ;
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]| )
A4: len f1 = 1 + 2 by FINSEQ_1:62;
A5: ( f1 /. 1 = |[0 ,0 ]| & f1 /. 2 = |[0 ,1]| & f1 /. 3 = |[1,1]| ) by FINSEQ_4:27;
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

( |[0 ,0 ]| <> |[0 ,1]| & |[0 ,1]| <> |[1,1]| & |[0 ,0 ]| <> |[1,1]| ) by A1, A3, EUCLID:56;
hence f1 is one-to-one by 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 A4; :: 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

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 A6: ( 1 <= i & i + 2 <= len f1 ) ; :: thesis: (LSeg f1,i) /\ (LSeg f1,(i + 1)) = {(f1 /. (i + 1))}
then i <= 1 by A4, XREAL_1:8;
then A7: i = 1 by A6, XXREAL_0:1;
1 + 1 in Seg (len f1) by A4, FINSEQ_1:3;
then A8: ( LSeg f1,1 = LSeg |[0 ,0 ]|,|[0 ,1]| & LSeg f1,(1 + 1) = LSeg |[0 ,1]|,|[1,1]| ) by A4, A5, Def5;
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 x in (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) ; :: thesis: x = |[0 ,1]|
then A9: ( x in { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } & 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 A10: ex p being Point of (TOP-REAL 2) st
( p = x & p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) ;
ex p2 being Point of (TOP-REAL 2) st
( p2 = x & p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 1 ) by A9;
hence x = |[0 ,1]| by A10, EUCLID:57; :: thesis: verum

end;

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

end;

hence (LSeg f1,i) /\ (LSeg f1,(i + 1)) = {(f1 /. (i + 1))} by A5, A7, A8, 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 A11: 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 A12: 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 A4, XREAL_1:8;
hence contradiction by A11, A12, 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 A13: ( 1 <= i & i + 1 <= len f1 ) ; :: thesis: ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 )
then A14: i <= 1 + 1 by A4, XREAL_1:8;

per cases ( i = 1 or i = 2 ) by A13, A14, NAT_1:9;

suppose A15: 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 A5, A15, EUCLID:56 ;
hence ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 ) ; :: thesis: verum

end;

suppose A16: 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 A5, A16, EUCLID:56 ;
hence ( (f1 /. i) `1 = (f1 /. (i + 1)) `1 or (f1 /. i) `2 = (f1 /. (i + 1)) `2 ) ; :: thesis: verum

end;

end;

end;

A17: L~ f1 = union {(LSeg |[0 ,0 ]|,|[0 ,1]|),(LSeg |[0 ,1]|,|[1,1]|)}

proof

( len f1 = 2 + 1 & 1 + 1 in Seg (len f1) ) by A4, FINSEQ_1:3;
then ( 1 + 1 <= len f1 & LSeg |[0 ,0 ]|,|[0 ,1]| = LSeg f1,1 ) by A5, Def5;
then A18: LSeg |[0 ,0 ]|,|[0 ,1]| in { (LSeg f1,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } ;
( 2 + 1 <= len f1 & LSeg |[0 ,1]|,|[1,1]| = LSeg f1,2 ) by A4, A5, Def5;
then LSeg |[0 ,1]|,|[1,1]| in { (LSeg f1,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f1 ) } ;
then A19: {(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 A18, ZFMISC_1:38;
{ (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
A20: ( a = LSeg f1,i & 1 <= i & i + 1 <= len f1 ) ;
i + 1 <= 2 + 1 by A20, FINSEQ_1:62;
then i <= 1 + 1 by XREAL_1:8;
then ( i = 1 or i = 2 ) by A20, NAT_1:9;
then ( a = LSeg |[0 ,0 ]|,|[0 ,1]| or a = LSeg |[0 ,1]|,|[1,1]| ) by A5, A20, Def5;
hence a in {(LSeg |[0 ,0 ]|,|[0 ,1]|),(LSeg |[0 ,1]|,|[1,1]|)} by TARSKI:def 2; :: thesis: verum

end;

hence union {(LSeg |[0 ,0 ]|,|[0 ,1]|),(LSeg |[0 ,1]|,|[1,1]|)} = L~ f1 by A19, XBOOLE_0:def 10; :: thesis: verum

end;

then A21: L~ f1 = (LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|) by ZFMISC_1:93;
A22: len f2 = 1 + 2 by FINSEQ_1:62;
A23: ( f2 /. 1 = |[0 ,0 ]| & f2 /. 2 = |[1,0 ]| & f2 /. 3 = |[1,1]| ) by FINSEQ_4:27;
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, A2, A3, 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 A22; :: 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

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 A24: ( 1 <= i & i + 2 <= len f2 ) ; :: thesis: (LSeg f2,i) /\ (LSeg f2,(i + 1)) = {(f2 /. (i + 1))}
then i <= 1 by A22, XREAL_1:8;
then A25: i = 1 by A24, XXREAL_0:1;
1 + 1 in Seg (len f2) by A22, FINSEQ_1:3;
then A26: ( LSeg f2,1 = LSeg |[0 ,0 ]|,|[1,0 ]| & LSeg f2,(1 + 1) = LSeg |[1,0 ]|,|[1,1]| ) by A22, A23, Def5;
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 x in (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) ; :: thesis: x = |[1,0 ]|
then A27: ( x in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } & 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 A28: ex p being Point of (TOP-REAL 2) st
( p = x & p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) ;
ex p2 being Point of (TOP-REAL 2) st
( p2 = x & p2 `1 = 1 & p2 `2 <= 1 & p2 `2 >= 0 ) by A27;
hence x = |[1,0 ]| by A28, EUCLID:57; :: thesis: verum

end;

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

end;

hence (LSeg f2,i) /\ (LSeg f2,(i + 1)) = {(f2 /. (i + 1))} by A23, A25, A26, 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 A29: 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 A30: 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 A22, XREAL_1:8;
hence contradiction by A29, A30, 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 A31: ( 1 <= i & i + 1 <= len f2 ) ; :: thesis: ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 )
then A32: i <= 1 + 1 by A22, XREAL_1:8;

per cases ( i = 1 or i = 2 ) by A31, A32, NAT_1:9;

suppose A33: 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 A23, A33, EUCLID:56 ;
hence ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 ) ; :: thesis: verum

end;

suppose A34: 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 A23, A34, EUCLID:56 ;
hence ( (f2 /. i) `1 = (f2 /. (i + 1)) `1 or (f2 /. i) `2 = (f2 /. (i + 1)) `2 ) ; :: thesis: verum

end;

end;

end;

A35: L~ f2 = union {(LSeg |[0 ,0 ]|,|[1,0 ]|),(LSeg |[1,0 ]|,|[1,1]|)}

proof

( len f2 = 2 + 1 & 1 + 1 in Seg (len f2) ) by A22, FINSEQ_1:3;
then ( 1 + 1 <= len f2 & LSeg |[0 ,0 ]|,|[1,0 ]| = LSeg f2,1 ) by A23, Def5;
then A36: LSeg |[0 ,0 ]|,|[1,0 ]| in { (LSeg f2,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } ;
( 2 + 1 <= len f2 & LSeg |[1,0 ]|,|[1,1]| = LSeg f2,2 ) by A22, A23, Def5;
then LSeg |[1,0 ]|,|[1,1]| in { (LSeg f2,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f2 ) } ;
then A37: {(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 A36, ZFMISC_1:38;
{ (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
A38: ( a = LSeg f2,i & 1 <= i & i + 1 <= len f2 ) ;
i + 1 <= 2 + 1 by A38, FINSEQ_1:62;
then i <= 1 + 1 by XREAL_1:8;
then ( i = 1 or i = 2 ) by A38, NAT_1:9;
then ( a = LSeg |[0 ,0 ]|,|[1,0 ]| or a = LSeg |[1,0 ]|,|[1,1]| ) by A23, A38, Def5;
hence a in {(LSeg |[0 ,0 ]|,|[1,0 ]|),(LSeg |[1,0 ]|,|[1,1]|)} by TARSKI:def 2; :: thesis: verum

end;

hence union {(LSeg |[0 ,0 ]|,|[1,0 ]|),(LSeg |[1,0 ]|,|[1,1]|)} = L~ f2 by A37, XBOOLE_0:def 10; :: thesis: verum

end;

then A39: L~ f2 = (LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|) by ZFMISC_1:93;
thus R^2-unit_square = (L~ f1) \/ (L~ f2) by A21, A35, 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]| )

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
A40: ( x in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } & x in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } ) by XBOOLE_0:3;
A41: ex p being Point of (TOP-REAL 2) st
( p = x & p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) by A40;
ex p2 being Point of (TOP-REAL 2) st
( p2 = x & p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 0 ) by A40;
hence contradiction by A41; :: thesis: verum

end;

then A42: { 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;
A43: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by Th26, XBOOLE_0:def 7;
thus (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 A17, A39, 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 A42, A43, 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 A4, A22, FINSEQ_4:27; :: thesis: verum