begin
definition
let p1,
p2,
p3 be ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ;
func angle (
p1,
p2,
p3)
-> ( ( ) (
complex V12()
ext-real )
Real)
equals
angle (
(euc2cpx p1 : ( ( ) ( ) RLTopStruct ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) ( non
empty V38()
V129()
V135() )
set ) ) ,
(euc2cpx p2 : ( ( ) ( ) Element of p1 : ( ( ) ( ) RLTopStruct ) ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) ( non
empty V38()
V129()
V135() )
set ) ) ,
(euc2cpx p3 : ( ( V21() V30(K7(p1 : ( ( ) ( ) RLTopStruct ) ,p1 : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,p1 : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(p1 : ( ( ) ( ) RLTopStruct ) ,p1 : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined p1 : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(p1 : ( ( ) ( ) RLTopStruct ) ,p1 : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,p1 : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(p1 : ( ( ) ( ) RLTopStruct ) ,p1 : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,p1 : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
complex )
Element of
COMPLEX : ( ( ) ( non
empty V38()
V129()
V135() )
set ) ) ) : ( (
V12() ) (
complex V12()
ext-real )
set ) ;
end;
theorem
for
p1,
p2,
p3 being ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) st
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
<> p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) &
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
<> p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) &
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
<> p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) &
angle (
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real)
< PI : ( ( ) (
complex V12()
ext-real )
Element of
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) holds
((angle (p2 : ( ( ) ( Relation-like V21() V45(2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) ,p1 : ( ( ) ( Relation-like V21() V45(2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) ,p3 : ( ( ) ( Relation-like V21() V45(2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( complex V12() ext-real ) Real) + (angle (p1 : ( ( ) ( Relation-like V21() V45(2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) ,p3 : ( ( ) ( Relation-like V21() V45(2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( Relation-like V21() V45(2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( complex V12() ext-real ) Real) ) : ( ( ) (
complex V12()
ext-real )
Element of
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) )
+ (angle (p3 : ( ( ) ( Relation-like V21() V45(2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( Relation-like V21() V45(2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) ,p1 : ( ( ) ( Relation-like V21() V45(2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( ) (
complex V12()
ext-real )
Real) : ( ( ) (
complex V12()
ext-real )
Element of
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) )
= PI : ( ( ) (
complex V12()
ext-real )
Element of
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) ;
definition
let n be ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) ;
let p1,
p2,
p3 be ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ;
func Triangle (
p1,
p2,
p3)
-> ( ( ) ( )
Subset of )
equals
((LSeg (p1 : ( ( ) ( ) Element of n : ( ( ) ( ) RLTopStruct ) ) ,p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) )) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( ( strict ) ( strict ) RLTopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) \/ (LSeg (p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) )) : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( ( strict ) ( strict ) RLTopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( )
Element of
K6( the
carrier of
(TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( (
strict ) (
strict )
RLTopStruct ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
\/ (LSeg (p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p1 : ( ( ) ( ) Element of n : ( ( ) ( ) RLTopStruct ) ) )) : ( ( ) ( )
Element of
K6( the
carrier of
(TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( (
strict ) (
strict )
RLTopStruct ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of
K6( the
carrier of
(TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( (
strict ) (
strict )
RLTopStruct ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ;
end;
definition
let n be ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) ;
let p1,
p2,
p3 be ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ;
func closed_inside_of_triangle (
p1,
p2,
p3)
-> ( ( ) ( )
Subset of )
equals
{ p : ( ( ) ( Relation-like V21() V45(n : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) where p is ( ( ) ( Relation-like V21() V45(n : ( ( ) ( ) RLTopStruct ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ex a1, a2, a3 being ( ( ) ( complex V12() ext-real ) Real) st
( 0 : ( ( ) ( empty natural complex V12() ext-real non positive non negative V33() V34() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) <= a1 : ( ( ) ( complex V12() ext-real ) Real) & 0 : ( ( ) ( empty natural complex V12() ext-real non positive non negative V33() V34() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) <= a2 : ( ( ) ( complex V12() ext-real ) Real) & 0 : ( ( ) ( empty natural complex V12() ext-real non positive non negative V33() V34() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) <= a3 : ( ( ) ( complex V12() ext-real ) Real) & (a1 : ( ( ) ( complex V12() ext-real ) Real) + a2 : ( ( ) ( complex V12() ext-real ) Real) ) : ( ( ) ( complex V12() ext-real ) Element of REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) + a3 : ( ( ) ( complex V12() ext-real ) Real) : ( ( ) ( complex V12() ext-real ) Element of REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) = 1 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) & p : ( ( ) ( Relation-like V21() V45(n : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) = ((a1 : ( ( ) ( complex V12() ext-real ) Real) * p1 : ( ( ) ( ) Element of n : ( ( ) ( ) RLTopStruct ) ) ) : ( ( ) ( ) Element of the carrier of (TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( ( strict ) ( strict ) RLTopStruct ) : ( ( ) ( ) set ) ) + (a2 : ( ( ) ( complex V12() ext-real ) Real) * p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of (TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( ( strict ) ( strict ) RLTopStruct ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of (TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( ( strict ) ( strict ) RLTopStruct ) : ( ( ) ( ) set ) ) + (a3 : ( ( ) ( complex V12() ext-real ) Real) * p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of (TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( ( strict ) ( strict ) RLTopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of (TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( ( strict ) ( strict ) RLTopStruct ) : ( ( ) ( ) set ) ) ) } ;
end;
definition
let n be ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) ;
let p1,
p2,
p3 be ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ;
func inside_of_triangle (
p1,
p2,
p3)
-> ( ( ) ( )
Subset of )
equals
(closed_inside_of_triangle (p1 : ( ( ) ( ) Element of n : ( ( ) ( ) RLTopStruct ) ) ,p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) )) : ( ( ) ( )
Subset of )
\ (Triangle (p1 : ( ( ) ( ) Element of n : ( ( ) ( ) RLTopStruct ) ) ,p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) )) : ( ( ) ( )
Subset of ) : ( ( ) ( )
Element of
K6( the
carrier of
(TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( (
strict ) (
strict )
RLTopStruct ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ;
end;
definition
let n be ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) ;
let p1,
p2,
p3 be ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ;
func outside_of_triangle (
p1,
p2,
p3)
-> ( ( ) ( )
Subset of )
equals
{ p : ( ( ) ( Relation-like V21() V45(n : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) where p is ( ( ) ( Relation-like V21() V45(n : ( ( ) ( ) RLTopStruct ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ex a1, a2, a3 being ( ( ) ( complex V12() ext-real ) Real) st
( ( 0 : ( ( ) ( empty natural complex V12() ext-real non positive non negative V33() V34() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) > a1 : ( ( ) ( complex V12() ext-real ) Real) or 0 : ( ( ) ( empty natural complex V12() ext-real non positive non negative V33() V34() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) > a2 : ( ( ) ( complex V12() ext-real ) Real) or 0 : ( ( ) ( empty natural complex V12() ext-real non positive non negative V33() V34() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) > a3 : ( ( ) ( complex V12() ext-real ) Real) ) & (a1 : ( ( ) ( complex V12() ext-real ) Real) + a2 : ( ( ) ( complex V12() ext-real ) Real) ) : ( ( ) ( complex V12() ext-real ) Element of REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) + a3 : ( ( ) ( complex V12() ext-real ) Real) : ( ( ) ( complex V12() ext-real ) Element of REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) = 1 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) & p : ( ( ) ( Relation-like V21() V45(n : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) = ((a1 : ( ( ) ( complex V12() ext-real ) Real) * p1 : ( ( ) ( ) Element of n : ( ( ) ( ) RLTopStruct ) ) ) : ( ( ) ( ) Element of the carrier of (TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( ( strict ) ( strict ) RLTopStruct ) : ( ( ) ( ) set ) ) + (a2 : ( ( ) ( complex V12() ext-real ) Real) * p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of (TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( ( strict ) ( strict ) RLTopStruct ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of (TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( ( strict ) ( strict ) RLTopStruct ) : ( ( ) ( ) set ) ) + (a3 : ( ( ) ( complex V12() ext-real ) Real) * p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of (TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( ( strict ) ( strict ) RLTopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of (TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( ( strict ) ( strict ) RLTopStruct ) : ( ( ) ( ) set ) ) ) } ;
end;
definition
let n be ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) ;
let p1,
p2,
p3 be ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ;
func plane (
p1,
p2,
p3)
-> ( ( ) ( )
Subset of )
equals
(outside_of_triangle (p1 : ( ( ) ( ) Element of n : ( ( ) ( ) RLTopStruct ) ) ,p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) )) : ( ( ) ( )
Subset of )
\/ (closed_inside_of_triangle (p1 : ( ( ) ( ) Element of n : ( ( ) ( ) RLTopStruct ) ) ,p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) )) : ( ( ) ( )
Subset of ) : ( ( ) ( )
Element of
K6( the
carrier of
(TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( (
strict ) (
strict )
RLTopStruct ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ;
end;
theorem
for
n being ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) )
for
p1,
p2,
p3,
p0 being ( ( ) (
Relation-like V21()
V45(
b1 : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) st
p2 : ( ( ) (
Relation-like V21()
V45(
b1 : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
- p1 : ( ( ) (
Relation-like V21()
V45(
b1 : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like V21()
V45(
b1 : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL b1 : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(
b1 : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
- p1 : ( ( ) (
Relation-like V21()
V45(
b1 : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like V21()
V45(
b1 : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL b1 : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) )
are_lindependent2 &
p0 : ( ( ) (
Relation-like V21()
V45(
b1 : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
in plane (
p1 : ( ( ) (
Relation-like V21()
V45(
b1 : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(
b1 : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(
b1 : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Subset of ) holds
ex
a1,
a2,
a3 being ( ( ) (
complex V12()
ext-real )
Real) st
(
p0 : ( ( ) (
Relation-like V21()
V45(
b1 : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
= ((a1 : ( ( ) ( complex V12() ext-real ) Real) * p1 : ( ( ) ( Relation-like V21() V45(b1 : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like V21() V45(b1 : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL b1 : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty V76() V141() V142() TopSpace-like V206() V207() V208() V209() V210() V211() V212() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) + (a2 : ( ( ) ( complex V12() ext-real ) Real) * p2 : ( ( ) ( Relation-like V21() V45(b1 : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like V21() V45(b1 : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL b1 : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty V76() V141() V142() TopSpace-like V206() V207() V208() V209() V210() V211() V212() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) (
Relation-like V21()
V45(
b1 : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL b1 : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) )
+ (a3 : ( ( ) ( complex V12() ext-real ) Real) * p3 : ( ( ) ( Relation-like V21() V45(b1 : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
Relation-like V21()
V45(
b1 : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL b1 : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like V21()
V45(
b1 : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL b1 : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) &
(a1 : ( ( ) ( complex V12() ext-real ) Real) + a2 : ( ( ) ( complex V12() ext-real ) Real) ) : ( ( ) (
complex V12()
ext-real )
Element of
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) )
+ a3 : ( ( ) (
complex V12()
ext-real )
Real) : ( ( ) (
complex V12()
ext-real )
Element of
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) )
= 1 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) & ( for
b1,
b2,
b3 being ( ( ) (
complex V12()
ext-real )
Real) st
p0 : ( ( ) (
Relation-like V21()
V45(
b1 : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
= ((b1 : ( ( ) ( complex V12() ext-real ) Real) * p1 : ( ( ) ( Relation-like V21() V45(b1 : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like V21() V45(b1 : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL b1 : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty V76() V141() V142() TopSpace-like V206() V207() V208() V209() V210() V211() V212() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) + (b2 : ( ( ) ( complex V12() ext-real ) Real) * p2 : ( ( ) ( Relation-like V21() V45(b1 : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like V21() V45(b1 : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL b1 : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty V76() V141() V142() TopSpace-like V206() V207() V208() V209() V210() V211() V212() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) (
Relation-like V21()
V45(
b1 : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL b1 : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) )
+ (b3 : ( ( ) ( complex V12() ext-real ) Real) * p3 : ( ( ) ( Relation-like V21() V45(b1 : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
Relation-like V21()
V45(
b1 : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL b1 : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like V21()
V45(
b1 : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL b1 : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) &
(b1 : ( ( ) ( complex V12() ext-real ) Real) + b2 : ( ( ) ( complex V12() ext-real ) Real) ) : ( ( ) (
complex V12()
ext-real )
Element of
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) )
+ b3 : ( ( ) (
complex V12()
ext-real )
Real) : ( ( ) (
complex V12()
ext-real )
Element of
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) )
= 1 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) holds
(
b1 : ( ( ) (
complex V12()
ext-real )
Real)
= a1 : ( ( ) (
complex V12()
ext-real )
Real) &
b2 : ( ( ) (
complex V12()
ext-real )
Real)
= a2 : ( ( ) (
complex V12()
ext-real )
Real) &
b3 : ( ( ) (
complex V12()
ext-real )
Real)
= a3 : ( ( ) (
complex V12()
ext-real )
Real) ) ) ) ;
definition
let n be ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) ;
let p1,
p2,
p3,
p be ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ;
assume
(
p2 : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
- p1 : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL n : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
- p1 : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL n : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) )
are_lindependent2 &
p : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
in plane (
p1 : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Subset of ) )
;
func tricord1 (
p1,
p2,
p3,
p)
-> ( ( ) (
complex V12()
ext-real )
Real)
means
ex
a2,
a3 being ( ( ) (
complex V12()
ext-real )
Real) st
(
(it : ( ( V21() V30(p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -valued V21() V30(p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) Element of K6(K7(p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) + a2 : ( ( ) ( complex V12() ext-real ) Real) ) : ( ( ) (
complex V12()
ext-real )
Element of
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) )
+ a3 : ( ( ) (
complex V12()
ext-real )
Real) : ( ( ) (
complex V12()
ext-real )
Element of
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) )
= 1 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) &
p : ( ( ) ( )
Element of
K6(
K6(
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
= ((it : ( ( V21() V30(p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -valued V21() V30(p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) Element of K6(K7(p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) * p1 : ( ( ) ( ) Element of n : ( ( ) ( ) RLTopStruct ) ) ) : ( ( ) ( ) Element of the carrier of (TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( ( strict ) ( strict ) RLTopStruct ) : ( ( ) ( ) set ) ) + (a2 : ( ( ) ( complex V12() ext-real ) Real) * p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of (TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( ( strict ) ( strict ) RLTopStruct ) : ( ( ) ( ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
(TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( (
strict ) (
strict )
RLTopStruct ) : ( ( ) ( )
set ) )
+ (a3 : ( ( ) ( complex V12() ext-real ) Real) * p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
(TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( (
strict ) (
strict )
RLTopStruct ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of the
carrier of
(TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( (
strict ) (
strict )
RLTopStruct ) : ( ( ) ( )
set ) ) );
end;
definition
let n be ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) ;
let p1,
p2,
p3,
p be ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ;
assume
(
p2 : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
- p1 : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL n : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
- p1 : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL n : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) )
are_lindependent2 &
p : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
in plane (
p1 : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Subset of ) )
;
func tricord2 (
p1,
p2,
p3,
p)
-> ( ( ) (
complex V12()
ext-real )
Real)
means
ex
a1,
a3 being ( ( ) (
complex V12()
ext-real )
Real) st
(
(a1 : ( ( ) ( complex V12() ext-real ) Real) + it : ( ( V21() V30(p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -valued V21() V30(p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) Element of K6(K7(p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
complex V12()
ext-real )
Element of
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) )
+ a3 : ( ( ) (
complex V12()
ext-real )
Real) : ( ( ) (
complex V12()
ext-real )
Element of
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) )
= 1 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) &
p : ( ( ) ( )
Element of
K6(
K6(
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
= ((a1 : ( ( ) ( complex V12() ext-real ) Real) * p1 : ( ( ) ( ) Element of n : ( ( ) ( ) RLTopStruct ) ) ) : ( ( ) ( ) Element of the carrier of (TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( ( strict ) ( strict ) RLTopStruct ) : ( ( ) ( ) set ) ) + (it : ( ( V21() V30(p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -valued V21() V30(p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) Element of K6(K7(p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) * p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of (TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( ( strict ) ( strict ) RLTopStruct ) : ( ( ) ( ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
(TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( (
strict ) (
strict )
RLTopStruct ) : ( ( ) ( )
set ) )
+ (a3 : ( ( ) ( complex V12() ext-real ) Real) * p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
(TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( (
strict ) (
strict )
RLTopStruct ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of the
carrier of
(TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( (
strict ) (
strict )
RLTopStruct ) : ( ( ) ( )
set ) ) );
end;
definition
let n be ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) ;
let p1,
p2,
p3,
p be ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ;
assume
(
p2 : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
- p1 : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL n : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
- p1 : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL n : ( ( ) ( natural complex V12() ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) )
are_lindependent2 &
p : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
in plane (
p1 : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(
n : ( ( ) (
natural complex V12()
ext-real V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Subset of ) )
;
func tricord3 (
p1,
p2,
p3,
p)
-> ( ( ) (
complex V12()
ext-real )
Real)
means
ex
a1,
a2 being ( ( ) (
complex V12()
ext-real )
Real) st
(
(a1 : ( ( ) ( complex V12() ext-real ) Real) + a2 : ( ( ) ( complex V12() ext-real ) Real) ) : ( ( ) (
complex V12()
ext-real )
Element of
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) )
+ it : ( (
V21()
V30(
p2 : ( (
V21()
V30(
K7(
n : ( ( ) ( )
RLTopStruct ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) ) (
Relation-like K7(
n : ( ( ) ( )
RLTopStruct ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set )
-defined n : ( ( ) ( )
RLTopStruct )
-valued V21()
V30(
K7(
n : ( ( ) ( )
RLTopStruct ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) )
Element of
K6(
K7(
K7(
n : ( ( ) ( )
RLTopStruct ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p3 : ( (
V21()
V30(
K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) ) (
Relation-like K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set )
-defined n : ( ( ) ( )
RLTopStruct )
-valued V21()
V30(
K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) ) (
Relation-like p2 : ( (
V21()
V30(
K7(
n : ( ( ) ( )
RLTopStruct ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) ) (
Relation-like K7(
n : ( ( ) ( )
RLTopStruct ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set )
-defined n : ( ( ) ( )
RLTopStruct )
-valued V21()
V30(
K7(
n : ( ( ) ( )
RLTopStruct ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) )
Element of
K6(
K7(
K7(
n : ( ( ) ( )
RLTopStruct ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
-defined p3 : ( (
V21()
V30(
K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) ) (
Relation-like K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set )
-defined n : ( ( ) ( )
RLTopStruct )
-valued V21()
V30(
K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
-valued V21()
V30(
p2 : ( (
V21()
V30(
K7(
n : ( ( ) ( )
RLTopStruct ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) ) (
Relation-like K7(
n : ( ( ) ( )
RLTopStruct ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set )
-defined n : ( ( ) ( )
RLTopStruct )
-valued V21()
V30(
K7(
n : ( ( ) ( )
RLTopStruct ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) )
Element of
K6(
K7(
K7(
n : ( ( ) ( )
RLTopStruct ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p3 : ( (
V21()
V30(
K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) ) (
Relation-like K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set )
-defined n : ( ( ) ( )
RLTopStruct )
-valued V21()
V30(
K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) )
Element of
K6(
K7(
p2 : ( (
V21()
V30(
K7(
n : ( ( ) ( )
RLTopStruct ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) ) (
Relation-like K7(
n : ( ( ) ( )
RLTopStruct ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set )
-defined n : ( ( ) ( )
RLTopStruct )
-valued V21()
V30(
K7(
n : ( ( ) ( )
RLTopStruct ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) )
Element of
K6(
K7(
K7(
n : ( ( ) ( )
RLTopStruct ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p3 : ( (
V21()
V30(
K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) ) (
Relation-like K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set )
-defined n : ( ( ) ( )
RLTopStruct )
-valued V21()
V30(
K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
complex V12()
ext-real )
Element of
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) )
= 1 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) &
p : ( ( ) ( )
Element of
K6(
K6(
n : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
= ((a1 : ( ( ) ( complex V12() ext-real ) Real) * p1 : ( ( ) ( ) Element of n : ( ( ) ( ) RLTopStruct ) ) ) : ( ( ) ( ) Element of the carrier of (TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( ( strict ) ( strict ) RLTopStruct ) : ( ( ) ( ) set ) ) + (a2 : ( ( ) ( complex V12() ext-real ) Real) * p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of (TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( ( strict ) ( strict ) RLTopStruct ) : ( ( ) ( ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
(TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( (
strict ) (
strict )
RLTopStruct ) : ( ( ) ( )
set ) )
+ (it : ( ( V21() V30(p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ( Relation-like p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -defined p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -valued V21() V30(p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) Element of K6(K7(p2 : ( ( V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(n : ( ( ) ( ) RLTopStruct ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) * p3 : ( ( V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) ( Relation-like K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) -defined n : ( ( ) ( ) RLTopStruct ) -valued V21() V30(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ,n : ( ( ) ( ) RLTopStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
(TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( (
strict ) (
strict )
RLTopStruct ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of the
carrier of
(TOP-REAL n : ( ( ) ( ) RLTopStruct ) ) : ( (
strict ) (
strict )
RLTopStruct ) : ( ( ) ( )
set ) ) );
end;
definition
let p1,
p2,
p3 be ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ;
func trcmap1 (
p1,
p2,
p3)
-> ( (
V21()
V30( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V204() )
TopStruct ) : ( ( ) ( non
empty V129()
V130()
V131() )
set ) ) ) (
Relation-like the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V204() )
TopStruct ) : ( ( ) ( non
empty V129()
V130()
V131() )
set )
-valued V21()
V30( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V204() )
TopStruct ) : ( ( ) ( non
empty V129()
V130()
V131() )
set ) )
complex-yielding V120()
V121() )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V129()
V130()
V131() )
set ) )
means
for
p being ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) holds
it : ( (
V21()
V30(
K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) ) (
Relation-like K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set )
-defined p1 : ( ( ) ( )
RLTopStruct )
-valued V21()
V30(
K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
. p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
complex V12()
ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V204() )
TopStruct ) : ( ( ) ( non
empty V129()
V130()
V131() )
set ) )
= tricord1 (
p1 : ( ( ) ( )
RLTopStruct ) ,
p2 : ( ( ) ( )
Element of
p1 : ( ( ) ( )
RLTopStruct ) ) ,
p3 : ( (
V21()
V30(
K7(
p1 : ( ( ) ( )
RLTopStruct ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) ) (
Relation-like K7(
p1 : ( ( ) ( )
RLTopStruct ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set )
-defined p1 : ( ( ) ( )
RLTopStruct )
-valued V21()
V30(
K7(
p1 : ( ( ) ( )
RLTopStruct ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) )
Element of
K6(
K7(
K7(
p1 : ( ( ) ( )
RLTopStruct ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real) ;
end;
definition
let p1,
p2,
p3 be ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ;
func trcmap2 (
p1,
p2,
p3)
-> ( (
V21()
V30( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V204() )
TopStruct ) : ( ( ) ( non
empty V129()
V130()
V131() )
set ) ) ) (
Relation-like the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V204() )
TopStruct ) : ( ( ) ( non
empty V129()
V130()
V131() )
set )
-valued V21()
V30( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V204() )
TopStruct ) : ( ( ) ( non
empty V129()
V130()
V131() )
set ) )
complex-yielding V120()
V121() )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V129()
V130()
V131() )
set ) )
means
for
p being ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) holds
it : ( (
V21()
V30(
K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) ) (
Relation-like K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set )
-defined p1 : ( ( ) ( )
RLTopStruct )
-valued V21()
V30(
K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
. p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
complex V12()
ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V204() )
TopStruct ) : ( ( ) ( non
empty V129()
V130()
V131() )
set ) )
= tricord2 (
p1 : ( ( ) ( )
RLTopStruct ) ,
p2 : ( ( ) ( )
Element of
p1 : ( ( ) ( )
RLTopStruct ) ) ,
p3 : ( (
V21()
V30(
K7(
p1 : ( ( ) ( )
RLTopStruct ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) ) (
Relation-like K7(
p1 : ( ( ) ( )
RLTopStruct ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set )
-defined p1 : ( ( ) ( )
RLTopStruct )
-valued V21()
V30(
K7(
p1 : ( ( ) ( )
RLTopStruct ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) )
Element of
K6(
K7(
K7(
p1 : ( ( ) ( )
RLTopStruct ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real) ;
end;
definition
let p1,
p2,
p3 be ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ;
func trcmap3 (
p1,
p2,
p3)
-> ( (
V21()
V30( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V204() )
TopStruct ) : ( ( ) ( non
empty V129()
V130()
V131() )
set ) ) ) (
Relation-like the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V204() )
TopStruct ) : ( ( ) ( non
empty V129()
V130()
V131() )
set )
-valued V21()
V30( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V204() )
TopStruct ) : ( ( ) ( non
empty V129()
V130()
V131() )
set ) )
complex-yielding V120()
V121() )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V129()
V130()
V131() )
set ) )
means
for
p being ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) holds
it : ( (
V21()
V30(
K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) ) (
Relation-like K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set )
-defined p1 : ( ( ) ( )
RLTopStruct )
-valued V21()
V30(
K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
. p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
complex V12()
ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V204() )
TopStruct ) : ( ( ) ( non
empty V129()
V130()
V131() )
set ) )
= tricord3 (
p1 : ( ( ) ( )
RLTopStruct ) ,
p2 : ( ( ) ( )
Element of
p1 : ( ( ) ( )
RLTopStruct ) ) ,
p3 : ( (
V21()
V30(
K7(
p1 : ( ( ) ( )
RLTopStruct ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) ) (
Relation-like K7(
p1 : ( ( ) ( )
RLTopStruct ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set )
-defined p1 : ( ( ) ( )
RLTopStruct )
-valued V21()
V30(
K7(
p1 : ( ( ) ( )
RLTopStruct ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) )
Element of
K6(
K7(
K7(
p1 : ( ( ) ( )
RLTopStruct ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ,
p1 : ( ( ) ( )
RLTopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real) ;
end;
theorem
for
p1,
p2,
p3,
p being ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) st
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
- p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
- p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) )
are_lindependent2 holds
(
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
in outside_of_triangle (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Subset of ) iff (
tricord1 (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real)
< 0 : ( ( ) (
empty natural complex V12()
ext-real non
positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) or
tricord2 (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real)
< 0 : ( ( ) (
empty natural complex V12()
ext-real non
positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) or
tricord3 (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real)
< 0 : ( ( ) (
empty natural complex V12()
ext-real non
positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) ) ) ;
theorem
for
p1,
p2,
p3,
p being ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) st
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
- p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
- p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) )
are_lindependent2 holds
(
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
in Triangle (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Subset of ) iff (
tricord1 (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real)
>= 0 : ( ( ) (
empty natural complex V12()
ext-real non
positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) &
tricord2 (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real)
>= 0 : ( ( ) (
empty natural complex V12()
ext-real non
positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) &
tricord3 (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real)
>= 0 : ( ( ) (
empty natural complex V12()
ext-real non
positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) & (
tricord1 (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real)
= 0 : ( ( ) (
empty natural complex V12()
ext-real non
positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) or
tricord2 (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real)
= 0 : ( ( ) (
empty natural complex V12()
ext-real non
positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) or
tricord3 (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real)
= 0 : ( ( ) (
empty natural complex V12()
ext-real non
positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) ) ) ) ;
theorem
for
p1,
p2,
p3,
p being ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) st
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
- p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
- p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) )
are_lindependent2 holds
(
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
in Triangle (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Subset of ) iff ( (
tricord1 (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real)
= 0 : ( ( ) (
empty natural complex V12()
ext-real non
positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) &
tricord2 (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real)
>= 0 : ( ( ) (
empty natural complex V12()
ext-real non
positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) &
tricord3 (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real)
>= 0 : ( ( ) (
empty natural complex V12()
ext-real non
positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) ) or (
tricord1 (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real)
>= 0 : ( ( ) (
empty natural complex V12()
ext-real non
positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) &
tricord2 (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real)
= 0 : ( ( ) (
empty natural complex V12()
ext-real non
positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) &
tricord3 (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real)
>= 0 : ( ( ) (
empty natural complex V12()
ext-real non
positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) ) or (
tricord1 (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real)
>= 0 : ( ( ) (
empty natural complex V12()
ext-real non
positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) &
tricord2 (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real)
>= 0 : ( ( ) (
empty natural complex V12()
ext-real non
positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) &
tricord3 (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real)
= 0 : ( ( ) (
empty natural complex V12()
ext-real non
positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) ) ) ) ;
theorem
for
p1,
p2,
p3,
p being ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) st
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
- p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
- p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural complex V12() ext-real positive non negative V33() V34() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( non empty V38() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty V76()
V141()
V142()
TopSpace-like V206()
V207()
V208()
V209()
V210()
V211()
V212()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) )
are_lindependent2 holds
(
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) )
in inside_of_triangle (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Subset of ) iff (
tricord1 (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real)
> 0 : ( ( ) (
empty natural complex V12()
ext-real non
positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) &
tricord2 (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real)
> 0 : ( ( ) (
empty natural complex V12()
ext-real non
positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) &
tricord3 (
p1 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p3 : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( ( ) (
Relation-like V21()
V45(2 : ( ( ) ( non
empty natural complex V12()
ext-real positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like complex-yielding V120()
V121() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
complex V12()
ext-real )
Real)
> 0 : ( ( ) (
empty natural complex V12()
ext-real non
positive non
negative V33()
V34()
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
NAT : ( ( ) (
V129()
V130()
V131()
V132()
V133()
V134()
V135() )
Element of
K6(
REAL : ( ( ) ( non
empty V38()
V129()
V130()
V131()
V135() )
set ) ) : ( ( ) ( )
set ) ) ) ) ) ;