:: TOPREAL2 semantic presentation

REAL is V162() V163() V164() V168() set
NAT is V162() V163() V164() V165() V166() V167() V168() Element of K19(REAL)
K19(REAL) is set
NAT is V162() V163() V164() V165() V166() V167() V168() set
K19(NAT) is set
K208() is non empty strict TopSpace-like TopStruct
the carrier of K208() is non empty set
1 is non empty V27() V28() ext-real positive non negative V110() V114() V115() V162() V163() V164() V165() V166() V167() Element of NAT
K20(1,1) is set
K19(K20(1,1)) is set
K20(K20(1,1),1) is set
K19(K20(K20(1,1),1)) is set
K20(K20(1,1),REAL) is set
K19(K20(K20(1,1),REAL)) is set
K20(REAL,REAL) is set
K20(K20(REAL,REAL),REAL) is set
K19(K20(K20(REAL,REAL),REAL)) is set
2 is non empty V27() V28() ext-real positive non negative V110() V114() V115() V162() V163() V164() V165() V166() V167() Element of NAT
K20(2,2) is set
K20(K20(2,2),REAL) is set
K19(K20(K20(2,2),REAL)) is set
K236() is V95() L7()
K246() is TopSpace-like TopStruct
K19(NAT) is set
COMPLEX is V162() V168() set
RAT is V162() V163() V164() V165() V168() set
INT is V162() V163() V164() V165() V166() V168() set
K19(K20(REAL,REAL)) is set
TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 V128() V174() V175() V176() V177() V178() V179() V180() strict RLTopStruct
the carrier of (TOP-REAL 2) is functional non empty set
K19( the carrier of (TOP-REAL 2)) is set
{} is Function-like functional empty V162() V163() V164() V165() V166() V167() V168() set
0 is Function-like functional empty V27() V28() ext-real non positive non negative V110() V114() V115() V162() V163() V164() V165() V166() V167() V168() Element of NAT
K112(0,1) is V162() V163() V164() Element of K19(REAL)
K247(0,1) is non empty strict TopSpace-like SubSpace of K246()
I[01] is non empty strict TopSpace-like SubSpace of K246()
the carrier of I[01] is non empty set
R^2-unit_square is functional non empty Element of K19( the carrier of (TOP-REAL 2))
|[0,0]| is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
|[0,1]| is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
LSeg (|[0,0]|,|[0,1]|) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
|[1,1]| is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
LSeg (|[0,1]|,|[1,1]|) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
|[1,0]| is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
LSeg (|[1,1]|,|[1,0]|) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[1,0]|,|[0,0]|) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 = 0 & b<sub>1</sub> `2 <= 1 & 0 <= b₁ `2 ) } is set
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 <= 1 & 0 <= b₁ `1 & b<sub>1</sub> `2 = 1 ) } is set
LSeg (|[0,0]|,|[1,0]|) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
{ b₁ where b₁ is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2) : ( b₁ `1 <= 1 & 0 <= b<sub>1</sub> `1 & b₁ `2 = 0 ) } is set
LSeg (|[1,0]|,|[1,1]|) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
{ b<sub>1</sub> where b<sub>1</sub> is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2) : ( b<sub>1</sub> `1 = 1 & b₁ `2 <= 1 & 0 <= b<sub>1</sub> `2 ) } is set
{ b₁ where b₁ is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2) : ( ( b₁ `1 = 0 & b<sub>1</sub> `2 <= 1 & 0 <= b₁ `2 ) or ( b<sub>1</sub> `1 <= 1 & 0 <= b₁ `1 & b<sub>1</sub> `2 = 1 ) or ( b₁ `1 <= 1 & 0 <= b<sub>1</sub> `1 & b₁ `2 = 0 ) or ( b<sub>1</sub> `1 = 1 & b₁ `2 <= 1 & 0 <= b<sub>1</sub> `2 ) ) } is set
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
{|[0,1]|} is functional non empty set
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
{|[1,0]|} is functional non empty set
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
{|[0,0]|} is functional non empty set
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
{|[1,1]|} is functional non empty set
{|[0,0]|,|[1,1]|} is functional non empty set
p00 is set
p01 is set
{p00} is non empty set
{p00} /\ p01 is set
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
|[0,0]| `1 is V28() ext-real V110() Element of REAL
|[0,0]| `2 is V28() ext-real V110() Element of REAL
|[0,1]| `1 is V28() ext-real V110() Element of REAL
|[0,1]| `2 is V28() ext-real V110() Element of REAL
|[1,0]| `1 is V28() ext-real V110() Element of REAL
|[1,0]| `2 is V28() ext-real V110() Element of REAL
|[1,1]| `1 is V28() ext-real V110() Element of REAL
|[1,1]| `2 is V28() ext-real V110() Element of REAL
P is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
f is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
{P,f} is functional non empty set
LSeg (|[0,0]|,P) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
LSeg (P,|[0,0]|) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,|[0,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[0,1]|,P) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,1]|,P)) /\ (LSeg (|[0,1]|,|[1,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
LSeg (P,|[0,1]|) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,1]|,P)) /\ (LSeg (|[1,0]|,|[1,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
R is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
R `1 is V28() ext-real V110() Element of REAL
R `2 is V28() ext-real V110() Element of REAL
LSeg (f,P) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
|[(R `1),(R `2)]| is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
S is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
S `1 is V28() ext-real V110() Element of REAL
S `2 is V28() ext-real V110() Element of REAL
|[(S `1),(S `2)]| is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
LSeg (P,f) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,f)) /\ (LSeg (P,|[0,0]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
{P} is functional non empty set
x is set
p1 is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
P `2 is V28() ext-real V110() Element of REAL
p1 `2 is V28() ext-real V110() Element of REAL
P `1 is V28() ext-real V110() Element of REAL
p1 `1 is V28() ext-real V110() Element of REAL
|[0,(P `2)]| is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
LSeg (|[0,1]|,f) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,1]|,f)) /\ (LSeg (|[0,1]|,|[1,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,|[0,0]|)) /\ (LSeg (|[0,1]|,f)) is functional Element of K19( the carrier of (TOP-REAL 2))
the Relation-like Function-like Element of (LSeg (P,|[0,0]|)) /\ (LSeg (|[0,1]|,f)) is Relation-like Function-like Element of (LSeg (P,|[0,0]|)) /\ (LSeg (|[0,1]|,f))
p1 is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
LSeg (f,|[0,1]|) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
f `2 is V28() ext-real V110() Element of REAL
p1 `2 is V28() ext-real V110() Element of REAL
P `2 is V28() ext-real V110() Element of REAL
(LSeg (|[0,1]|,f)) /\ (LSeg (|[0,0]|,|[1,0]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,f)) /\ (LSeg (|[0,0]|,|[1,0]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,f)) /\ (LSeg (|[0,1]|,f)) is functional Element of K19( the carrier of (TOP-REAL 2))
{f} is functional non empty set
x is set
p1 is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
p1 `2 is V28() ext-real V110() Element of REAL
P `1 is V28() ext-real V110() Element of REAL
p1 `1 is V28() ext-real V110() Element of REAL
|[0,(f `2)]| is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
(LSeg (P,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[1,1]|,|[0,1]|) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,f)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,f))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) /\ (LSeg (|[1,1]|,|[0,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
{} \/ {|[1,1]|} is non empty set
(((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) /\ (LSeg (|[0,1]|,f)) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,1]|,f)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,1]|,f)) /\ (LSeg (|[1,1]|,|[0,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (|[0,1]|,f)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (|[0,1]|,f)) /\ (LSeg (|[1,1]|,|[0,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,1]|,f)) /\ (LSeg (|[1,0]|,|[1,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
{} \/ ((LSeg (|[0,1]|,f)) /\ (LSeg (|[1,0]|,|[1,1]|))) is set
({} \/ ((LSeg (|[0,1]|,f)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (|[0,1]|,f)) /\ (LSeg (|[1,1]|,|[0,1]|))) is set
{} \/ ((LSeg (|[0,1]|,f)) /\ (LSeg (|[1,1]|,|[0,1]|))) is set
(LSeg (P,|[0,0]|)) /\ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,f))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,|[0,0]|)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P,|[0,0]|)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (P,|[0,0]|)) /\ (LSeg (|[0,1]|,f))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,|[0,0]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,|[0,0]|)) /\ (LSeg (|[1,1]|,|[0,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P,|[0,0]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (P,|[0,0]|)) /\ (LSeg (|[1,1]|,|[0,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
(((LSeg (P,|[0,0]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (P,|[0,0]|)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (P,|[0,0]|)) /\ (LSeg (|[0,1]|,f))) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P,|[0,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (P,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
(((LSeg (P,|[0,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (P,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (P,|[0,0]|)) /\ (LSeg (|[1,1]|,|[0,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
((((LSeg (P,|[0,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (P,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (P,|[0,0]|)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (P,|[0,0]|)) /\ (LSeg (|[0,1]|,f))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,1]|,f)) \/ (LSeg (f,P)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
((LSeg (|[0,1]|,f)) \/ (LSeg (f,P))) \/ (LSeg (P,|[0,0]|)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,f)) \/ (LSeg (|[0,1]|,f)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P,f)) \/ (LSeg (|[0,1]|,f))) \/ (LSeg (P,|[0,0]|)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(((LSeg (P,f)) \/ (LSeg (|[0,1]|,f))) \/ (LSeg (P,|[0,0]|))) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,|[0,0]|)) \/ (LSeg (|[0,1]|,f)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,f)) \/ ((LSeg (P,|[0,0]|)) \/ (LSeg (|[0,1]|,f))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P,f)) \/ ((LSeg (P,|[0,0]|)) \/ (LSeg (|[0,1]|,f)))) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P,|[0,0]|)) \/ (LSeg (|[0,1]|,f))) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,f)) \/ (((LSeg (P,|[0,0]|)) \/ (LSeg (|[0,1]|,f))) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|)))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,f)) \/ ((LSeg (P,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,f)))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,f)) /\ ((LSeg (P,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,f)))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,f)) /\ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,f))) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P,f)) /\ (LSeg (P,|[0,0]|))) \/ ((LSeg (P,f)) /\ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,f)))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,f)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P,f)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (P,f)) /\ (LSeg (|[0,1]|,f))) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P,f)) /\ (LSeg (P,|[0,0]|))) \/ (((LSeg (P,f)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (P,f)) /\ (LSeg (|[0,1]|,f)))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,f)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,f)) /\ (LSeg (|[1,1]|,|[0,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P,f)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (P,f)) /\ (LSeg (|[1,1]|,|[0,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
(((LSeg (P,f)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (P,f)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (P,f)) /\ (LSeg (|[0,1]|,f))) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P,f)) /\ (LSeg (P,|[0,0]|))) \/ ((((LSeg (P,f)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (P,f)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (P,f)) /\ (LSeg (|[0,1]|,f)))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,f)) /\ (LSeg (|[1,0]|,|[1,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P,f)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (P,f)) /\ (LSeg (|[1,0]|,|[1,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
(((LSeg (P,f)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (P,f)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (P,f)) /\ (LSeg (|[1,1]|,|[0,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
((((LSeg (P,f)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (P,f)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (P,f)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (P,f)) /\ (LSeg (|[0,1]|,f))) is functional Element of K19( the carrier of (TOP-REAL 2))
{P} \/ (((((LSeg (P,f)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (P,f)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (P,f)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (P,f)) /\ (LSeg (|[0,1]|,f)))) is non empty set
((LSeg (P,f)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {} is set
(((LSeg (P,f)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {}) \/ ((LSeg (P,f)) /\ (LSeg (|[1,1]|,|[0,1]|))) is set
((((LSeg (P,f)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {}) \/ ((LSeg (P,f)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (P,f)) /\ (LSeg (|[0,1]|,f))) is set
{P} \/ (((((LSeg (P,f)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {}) \/ ((LSeg (P,f)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (P,f)) /\ (LSeg (|[0,1]|,f)))) is non empty set
(LSeg (P,f)) /\ (LSeg (|[0,1]|,|[1,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P,f)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {f} is non empty set
((LSeg (P,f)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ (((LSeg (P,f)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {f}) is non empty set
{P} \/ (((LSeg (P,f)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ (((LSeg (P,f)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {f})) is non empty set
{P} \/ ((LSeg (P,f)) /\ (LSeg (|[0,0]|,|[1,0]|))) is non empty set
({P} \/ ((LSeg (P,f)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ (((LSeg (P,f)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {f}) is non empty set
{P} \/ (((LSeg (P,f)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {f}) is non empty set
{P} \/ (((LSeg (P,f)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {f}) is non empty set
{P} \/ (((LSeg (P,f)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {f}) is non empty set
{P} \/ (((LSeg (P,f)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {f}) is non empty set
f `1 is V28() ext-real V110() Element of REAL
|[(f `1),(f `2)]| is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
(LSeg (f,P)) /\ (LSeg (|[0,1]|,P)) is functional Element of K19( the carrier of (TOP-REAL 2))
{P} is functional non empty set
x is set
p1 is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
P `2 is V28() ext-real V110() Element of REAL
p1 `2 is V28() ext-real V110() Element of REAL
f `1 is V28() ext-real V110() Element of REAL
p1 `1 is V28() ext-real V110() Element of REAL
|[0,(P `2)]| is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
LSeg (f,|[0,0]|) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
(LSeg (f,|[0,0]|)) /\ (LSeg (|[0,1]|,P)) is functional Element of K19( the carrier of (TOP-REAL 2))
the Relation-like Function-like Element of (LSeg (f,|[0,0]|)) /\ (LSeg (|[0,1]|,P)) is Relation-like Function-like Element of (LSeg (f,|[0,0]|)) /\ (LSeg (|[0,1]|,P))
p1 is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
LSeg (|[0,0]|,f) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
P `2 is V28() ext-real V110() Element of REAL
p1 `2 is V28() ext-real V110() Element of REAL
f `2 is V28() ext-real V110() Element of REAL
(LSeg (f,P)) /\ (LSeg (|[0,0]|,|[1,0]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (f,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (f,|[0,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,1]|,P)) /\ (LSeg (|[0,0]|,|[1,0]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (f,P)) /\ (LSeg (f,|[0,0]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
{f} is functional non empty set
x is set
p1 is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
p1 `2 is V28() ext-real V110() Element of REAL
f `1 is V28() ext-real V110() Element of REAL
p1 `1 is V28() ext-real V110() Element of REAL
|[0,(f `2)]| is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
LSeg (|[1,1]|,|[0,1]|) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,P)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (f,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,P))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
x is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,1]|,|[1,1]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
{} \/ {|[1,1]|} is non empty set
(LSeg (P,|[0,1]|)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,1]|,P)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,1]|,P)) /\ (LSeg (|[1,1]|,|[0,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (|[0,1]|,P)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (|[0,1]|,P)) /\ (LSeg (|[1,1]|,|[0,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (|[0,1]|,P)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (|[0,1]|,P)) /\ (LSeg (|[1,0]|,|[1,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
(((LSeg (|[0,1]|,P)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (|[0,1]|,P)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (|[0,1]|,P)) /\ (LSeg (|[1,1]|,|[0,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
{} \/ ((LSeg (|[0,1]|,P)) /\ (LSeg (|[1,0]|,|[1,1]|))) is set
({} \/ ((LSeg (|[0,1]|,P)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (|[0,1]|,P)) /\ (LSeg (|[1,1]|,|[0,1]|))) is set
((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,P))) /\ (LSeg (|[0,0]|,f)) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (f,|[0,0]|)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (f,|[0,0]|)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (f,|[0,0]|)) /\ (LSeg (|[0,1]|,P))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (f,|[0,0]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (f,|[0,0]|)) /\ (LSeg (|[1,1]|,|[0,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (f,|[0,0]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (f,|[0,0]|)) /\ (LSeg (|[1,1]|,|[0,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
(((LSeg (f,|[0,0]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (f,|[0,0]|)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (f,|[0,0]|)) /\ (LSeg (|[0,1]|,P))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (f,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (f,|[0,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (f,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
(((LSeg (f,|[0,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (f,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (f,|[0,0]|)) /\ (LSeg (|[1,1]|,|[0,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
((((LSeg (f,|[0,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (f,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (f,|[0,0]|)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (f,|[0,0]|)) /\ (LSeg (|[0,1]|,P))) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (f,|[0,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {} is set
(((LSeg (f,|[0,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {}) \/ ((LSeg (f,|[0,0]|)) /\ (LSeg (|[1,1]|,|[0,1]|))) is set
((((LSeg (f,|[0,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {}) \/ ((LSeg (f,|[0,0]|)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (f,|[0,0]|)) /\ (LSeg (|[0,1]|,P))) is set
p1 is functional non empty Element of K19( the carrier of (TOP-REAL 2))
LSeg (P,f) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,1]|,P)) \/ (LSeg (P,f)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
((LSeg (|[0,1]|,P)) \/ (LSeg (P,f))) \/ (LSeg (f,|[0,0]|)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (f,P)) \/ (LSeg (|[0,1]|,P)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
((LSeg (f,P)) \/ (LSeg (|[0,1]|,P))) \/ (LSeg (f,|[0,0]|)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(((LSeg (f,P)) \/ (LSeg (|[0,1]|,P))) \/ (LSeg (f,|[0,0]|))) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (f,|[0,0]|)) \/ (LSeg (|[0,1]|,P)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (f,P)) \/ ((LSeg (f,|[0,0]|)) \/ (LSeg (|[0,1]|,P))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
((LSeg (f,P)) \/ ((LSeg (f,|[0,0]|)) \/ (LSeg (|[0,1]|,P)))) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
((LSeg (f,|[0,0]|)) \/ (LSeg (|[0,1]|,P))) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (f,P)) \/ (((LSeg (f,|[0,0]|)) \/ (LSeg (|[0,1]|,P))) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|)))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
x \/ p1 is functional non empty Element of K19( the carrier of (TOP-REAL 2))
x /\ p1 is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (f,P)) /\ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,P))) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (f,P)) /\ (LSeg (f,|[0,0]|))) \/ ((LSeg (f,P)) /\ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,P)))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (f,P)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (f,P)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (f,P)) /\ (LSeg (|[0,1]|,P))) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (f,P)) /\ (LSeg (f,|[0,0]|))) \/ (((LSeg (f,P)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (f,P)) /\ (LSeg (|[0,1]|,P)))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (f,P)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (f,P)) /\ (LSeg (|[1,1]|,|[0,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (f,P)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (f,P)) /\ (LSeg (|[1,1]|,|[0,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
(((LSeg (f,P)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (f,P)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (f,P)) /\ (LSeg (|[0,1]|,P))) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (f,P)) /\ (LSeg (f,|[0,0]|))) \/ ((((LSeg (f,P)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (f,P)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (f,P)) /\ (LSeg (|[0,1]|,P)))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (f,P)) /\ (LSeg (|[1,0]|,|[1,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (f,P)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (f,P)) /\ (LSeg (|[1,0]|,|[1,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
(((LSeg (f,P)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (f,P)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (f,P)) /\ (LSeg (|[1,1]|,|[0,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
((((LSeg (f,P)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (f,P)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (f,P)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (f,P)) /\ (LSeg (|[0,1]|,P))) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (f,P)) /\ (LSeg (f,|[0,0]|))) \/ (((((LSeg (f,P)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (f,P)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (f,P)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (f,P)) /\ (LSeg (|[0,1]|,P)))) is functional Element of K19( the carrier of (TOP-REAL 2))
{f} \/ (((((LSeg (f,P)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (f,P)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (f,P)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (f,P)) /\ (LSeg (|[0,1]|,P)))) is non empty set
((LSeg (f,P)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {} is set
(((LSeg (f,P)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {}) \/ ((LSeg (f,P)) /\ (LSeg (|[1,1]|,|[0,1]|))) is set
((((LSeg (f,P)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {}) \/ ((LSeg (f,P)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (f,P)) /\ (LSeg (|[0,1]|,P))) is set
{f} \/ (((((LSeg (f,P)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {}) \/ ((LSeg (f,P)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (f,P)) /\ (LSeg (|[0,1]|,P)))) is non empty set
(LSeg (f,P)) /\ (LSeg (|[0,1]|,|[1,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (f,P)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (f,P)) /\ (LSeg (|[0,1]|,|[1,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
(((LSeg (f,P)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (f,P)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ {P} is non empty set
{f} \/ ((((LSeg (f,P)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (f,P)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ {P}) is non empty set
((LSeg (f,P)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {P} is non empty set
((LSeg (f,P)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ (((LSeg (f,P)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {P}) is non empty set
{f} \/ (((LSeg (f,P)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ (((LSeg (f,P)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {P})) is non empty set
{f} \/ ((LSeg (f,P)) /\ (LSeg (|[0,0]|,|[1,0]|))) is non empty set
({f} \/ ((LSeg (f,P)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ (((LSeg (f,P)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {P}) is non empty set
{f} \/ (((LSeg (f,P)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {P}) is non empty set
{f} \/ (((LSeg (f,P)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {P}) is non empty set
{f} \/ (((LSeg (f,P)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {P}) is non empty set
{f} \/ (((LSeg (f,P)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {P}) is non empty set
P `1 is V28() ext-real V110() Element of REAL
|[(P `1),(P `2)]| is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
LSeg (P,f) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[1,1]|,|[0,1]|) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[0,1]|,f) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
(((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,f)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,f))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,f)) \/ ((LSeg (P,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,f)))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,f)) /\ ((LSeg (P,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,f)))) is functional Element of K19( the carrier of (TOP-REAL 2))
LSeg (P,f) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[1,1]|,|[0,1]|) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[0,1]|,f) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
(((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,f)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,f))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,f)) \/ ((LSeg (P,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,f)))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,f)) /\ ((LSeg (P,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,f)))) is functional Element of K19( the carrier of (TOP-REAL 2))
x is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
p1 is functional non empty Element of K19( the carrier of (TOP-REAL 2))
x \/ p1 is functional non empty Element of K19( the carrier of (TOP-REAL 2))
x /\ p1 is functional Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[0,1]|,f) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,|[0,1]|)) /\ (LSeg (|[0,1]|,f)) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,|[0,1]|)) \/ (LSeg (|[0,1]|,f)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
S is functional non empty Element of K19( the carrier of (TOP-REAL 2))
LSeg (|[1,1]|,f) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,f)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,|[0,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,f))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
x is functional non empty Element of K19( the carrier of (TOP-REAL 2))
S \/ x is functional non empty Element of K19( the carrier of (TOP-REAL 2))
S /\ x is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[1,1]|,f)) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,|[0,1]|)) \/ (LSeg (P,|[0,0]|)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,1]|,f)) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) /\ (LSeg (|[1,1]|,f)) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,1]|,f))) \/ ((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[1,1]|,f))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,1]|,f)) /\ (LSeg (|[1,1]|,f)) is functional Element of K19( the carrier of (TOP-REAL 2))
{f} is functional non empty set
(LSeg (|[1,1]|,f)) \/ (LSeg (|[0,1]|,f)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,|[0,0]|)) /\ (LSeg (|[1,1]|,f)) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,1]|,f)) /\ (LSeg (|[0,0]|,|[1,0]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
f `1 is V28() ext-real V110() Element of REAL
p1 is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
p1 `1 is V28() ext-real V110() Element of REAL
p1 `2 is V28() ext-real V110() Element of REAL
LSeg (f,|[1,1]|) is functional non empty V210( TOP-REAL 2) Element of K19( the carrier of (TOP-REAL 2))
p1 is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
p1 `1 is V28() ext-real V110() Element of REAL
p1 `2 is V28() ext-real V110() Element of REAL
P `2 is V28() ext-real V110() Element of REAL
|[(|[0,1]| `1),(|[0,1]| `2)]| is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
p1 is Relation-like Function-like V42(2) FinSequence-like V154() Element of the carrier of (TOP-REAL 2)
p1 `1 is V28() ext-real V110() Element of REAL
p1 `2 is V28() ext-real V110() Element of REAL
(LSeg (P,|[0,0]|)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,f))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,|[0,0]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P,|[0,0]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (P,|[0,0]|)) /\ (LSeg (|[1,1]|,f))) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P,|[0,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (P,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,|[0,1]|)) \/ ((LSeg (P,|[0,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,f)))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,1]|,f)) \/ ((LSeg (P,|[0,1]|)) \/ ((LSeg (P,|[0,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,f))))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,0]|,|[0,1]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,f))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
((LSeg (|[0,0]|,|[0,1]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,f)))) \/ (LSeg (|[0,1]|,f)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,f))) \/ (LSeg (|[0,1]|,f)) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,0]|,|[0,1]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,f))) \/ (LSeg (|[0,1]|,f))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,1]|,|[1,1]|)) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,0]|,|[0,1]|)) \/ ((LSeg (|[0,1]|,|[1,1]|)) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) is functional non empty Element of K19( the carrier of (TOP-REAL 2))
{P} is functional non empty set
(LSeg (P,|[0,1]|)) /\ (LSeg (P,|[0,0]|)) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,|[0,1]|)) /\ ((LSeg (P,|[0,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,f)))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (|[0,1]|,f)) /\ ((LSeg (P,|[0,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,f)))) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P,|[0,1]|)) /\ ((LSeg (P,|[0,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,f))))) \/ ((LSeg (|[0,1]|,f)) /\ ((LSeg (P,|[0,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,f))))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,|[0,1]|)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,f))) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P,|[0,1]|)) /\ (LSeg (P,|[0,0]|))) \/ ((LSeg (P,|[0,1]|)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,f)))) is functional Element of K19( the carrier of (TOP-REAL 2))
(((LSeg (P,|[0,1]|)) /\ (LSeg (P,|[0,0]|))) \/ ((LSeg (P,|[0,1]|)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,f))))) \/ ((LSeg (|[0,1]|,f)) /\ ((LSeg (P,|[0,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,f))))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,|[0,1]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) is functional Element of K19( the carrier of (TOP-REAL 2))
(LSeg (P,|[0,1]|)) /\ (LSeg (|[1,1]|,f)) is functional Element of K19( the carrier of (TOP-REAL 2))
((LSeg (P,|[0,1]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (P,|[0,1]|)) /\ (LSeg (|[1,1]|,f))) is functional Element of K19( the carrier of (TOP-REAL 2))
{P} \/ (((LSeg (P,|[0,1]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (P,|[0,1]|)) /\ (LSeg (|[1,1]|,f)))) is non empty set
({P}