:: EUCLID_5 semantic presentation

begin

theorem :: EUCLID_5:1
for p being ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ex x, y, z being ( ( ) ( V11() real V116() ) Real) st p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) = <*x : ( ( ) ( V11() real V116() ) Real) ,y : ( ( ) ( V11() real V116() ) Real) ,z : ( ( ) ( V11() real V116() ) Real) *> : ( ( ) ( V13() V16( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) Function-like FinSequence-like complex-yielding V120() V121() ) FinSequence of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ;

definition
let p be ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ;
func p `1 -> ( ( ) ( V11() real V116() ) Real) equals :: EUCLID_5:def 1
p : ( ( ) ( ) 2-sorted ) . 1 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ;
func p `2 -> ( ( ) ( V11() real V116() ) Real) equals :: EUCLID_5:def 2
p : ( ( ) ( ) 2-sorted ) . 2 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ;
func p `3 -> ( ( ) ( V11() real V116() ) Real) equals :: EUCLID_5:def 3
p : ( ( ) ( ) 2-sorted ) . 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ;
end;

notation
let x, y, z be ( ( real ) ( V11() real V116() ) number ) ;
synonym |[x,y,z]| for <*x,y,z*>;
end;

definition
let x, y, z be ( ( real ) ( V11() real V116() ) number ) ;
:: original: |[
redefine func |[x,y,z]| -> ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ;
end;

theorem :: EUCLID_5:2
for x, y, z being ( ( ) ( V11() real V116() ) Real) holds
( |[x : ( ( ) ( V11() real V116() ) Real) ,y : ( ( ) ( V11() real V116() ) Real) ,z : ( ( ) ( V11() real V116() ) Real) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `1 : ( ( ) ( V11() real V116() ) Real) = x : ( ( ) ( V11() real V116() ) Real) & |[x : ( ( ) ( V11() real V116() ) Real) ,y : ( ( ) ( V11() real V116() ) Real) ,z : ( ( ) ( V11() real V116() ) Real) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `2 : ( ( ) ( V11() real V116() ) Real) = y : ( ( ) ( V11() real V116() ) Real) & |[x : ( ( ) ( V11() real V116() ) Real) ,y : ( ( ) ( V11() real V116() ) Real) ,z : ( ( ) ( V11() real V116() ) Real) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `3 : ( ( ) ( V11() real V116() ) Real) = z : ( ( ) ( V11() real V116() ) Real) ) ;

theorem :: EUCLID_5:3
for p being ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) holds p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) = |[(p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `1) : ( ( ) ( V11() real V116() ) Real) ,(p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `2) : ( ( ) ( V11() real V116() ) Real) ,(p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `3) : ( ( ) ( V11() real V116() ) Real) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ;

theorem :: EUCLID_5:4
0. (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) = |[0 : ( ( ) ( natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ,0 : ( ( ) ( natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ,0 : ( ( ) ( natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ;

theorem :: EUCLID_5:5
for p1, p2 being ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) holds p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) + p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) = |[((p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `1) : ( ( ) ( V11() real V116() ) Real) + (p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `1) : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,((p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `2) : ( ( ) ( V11() real V116() ) Real) + (p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `2) : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,((p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `3) : ( ( ) ( V11() real V116() ) Real) + (p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `3) : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ;

theorem :: EUCLID_5:6
for x1, y1, z1, x2, y2, z2 being ( ( ) ( V11() real V116() ) Real) holds |[x1 : ( ( ) ( V11() real V116() ) Real) ,y1 : ( ( ) ( V11() real V116() ) Real) ,z1 : ( ( ) ( V11() real V116() ) Real) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) + |[x2 : ( ( ) ( V11() real V116() ) Real) ,y2 : ( ( ) ( V11() real V116() ) Real) ,z2 : ( ( ) ( V11() real V116() ) Real) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) = |[(x1 : ( ( ) ( V11() real V116() ) Real) + x2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,(y1 : ( ( ) ( V11() real V116() ) Real) + y2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,(z1 : ( ( ) ( V11() real V116() ) Real) + z2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ;

theorem :: EUCLID_5:7
for x being ( ( ) ( V11() real V116() ) Real)
for p being ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) holds x : ( ( ) ( V11() real V116() ) Real) * p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) = |[(x : ( ( ) ( V11() real V116() ) Real) * (p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `1) : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,(x : ( ( ) ( V11() real V116() ) Real) * (p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `2) : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,(x : ( ( ) ( V11() real V116() ) Real) * (p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `3) : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ;

theorem :: EUCLID_5:8
for x, x1, y1, z1 being ( ( ) ( V11() real V116() ) Real) holds x : ( ( ) ( V11() real V116() ) Real) * |[x1 : ( ( ) ( V11() real V116() ) Real) ,y1 : ( ( ) ( V11() real V116() ) Real) ,z1 : ( ( ) ( V11() real V116() ) Real) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) = |[(x : ( ( ) ( V11() real V116() ) Real) * x1 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,(x : ( ( ) ( V11() real V116() ) Real) * y1 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,(x : ( ( ) ( V11() real V116() ) Real) * z1 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ;

theorem :: EUCLID_5:9
for x being ( ( ) ( V11() real V116() ) Real)
for p being ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) holds
( (x : ( ( ) ( V11() real V116() ) Real) * p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) `1 : ( ( ) ( V11() real V116() ) Real) = x : ( ( ) ( V11() real V116() ) Real) * (p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `1) : ( ( ) ( V11() real V116() ) Real) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) & (x : ( ( ) ( V11() real V116() ) Real) * p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) `2 : ( ( ) ( V11() real V116() ) Real) = x : ( ( ) ( V11() real V116() ) Real) * (p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `2) : ( ( ) ( V11() real V116() ) Real) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) & (x : ( ( ) ( V11() real V116() ) Real) * p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) `3 : ( ( ) ( V11() real V116() ) Real) = x : ( ( ) ( V11() real V116() ) Real) * (p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `3) : ( ( ) ( V11() real V116() ) Real) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ) ;

theorem :: EUCLID_5:10
for p being ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) holds - p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) = |[(- (p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `1) : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,(- (p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `2) : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,(- (p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `3) : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ;

theorem :: EUCLID_5:11
for x1, y1, z1 being ( ( ) ( V11() real V116() ) Real) holds - |[x1 : ( ( ) ( V11() real V116() ) Real) ,y1 : ( ( ) ( V11() real V116() ) Real) ,z1 : ( ( ) ( V11() real V116() ) Real) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) = |[(- x1 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,(- y1 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,(- z1 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ;

theorem :: EUCLID_5:12
for p1, p2 being ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) holds p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) - p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) = |[((p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `1) : ( ( ) ( V11() real V116() ) Real) - (p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `1) : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,((p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `2) : ( ( ) ( V11() real V116() ) Real) - (p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `2) : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,((p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `3) : ( ( ) ( V11() real V116() ) Real) - (p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `3) : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ;

theorem :: EUCLID_5:13
for x1, y1, z1, x2, y2, z2 being ( ( ) ( V11() real V116() ) Real) holds |[x1 : ( ( ) ( V11() real V116() ) Real) ,y1 : ( ( ) ( V11() real V116() ) Real) ,z1 : ( ( ) ( V11() real V116() ) Real) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) - |[x2 : ( ( ) ( V11() real V116() ) Real) ,y2 : ( ( ) ( V11() real V116() ) Real) ,z2 : ( ( ) ( V11() real V116() ) Real) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) = |[(x1 : ( ( ) ( V11() real V116() ) Real) - x2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,(y1 : ( ( ) ( V11() real V116() ) Real) - y2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,(z1 : ( ( ) ( V11() real V116() ) Real) - z2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ;

definition
let p1, p2 be ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ;
func p1 <X> p2 -> ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) equals :: EUCLID_5:def 4
|[(((p1 : ( ( ) ( ) 2-sorted ) `2) : ( ( ) ( V11() real V116() ) Real) * (p2 : ( ( ) ( ) set ) `3) : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) - ((p1 : ( ( ) ( ) 2-sorted ) `3) : ( ( ) ( V11() real V116() ) Real) * (p2 : ( ( ) ( ) set ) `2) : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,(((p1 : ( ( ) ( ) 2-sorted ) `3) : ( ( ) ( V11() real V116() ) Real) * (p2 : ( ( ) ( ) set ) `1) : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) - ((p1 : ( ( ) ( ) 2-sorted ) `1) : ( ( ) ( V11() real V116() ) Real) * (p2 : ( ( ) ( ) set ) `3) : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,(((p1 : ( ( ) ( ) 2-sorted ) `1) : ( ( ) ( V11() real V116() ) Real) * (p2 : ( ( ) ( ) set ) `2) : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) - ((p1 : ( ( ) ( ) 2-sorted ) `2) : ( ( ) ( V11() real V116() ) Real) * (p2 : ( ( ) ( ) set ) `1) : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ;
end;

theorem :: EUCLID_5:14
for x, y, z being ( ( ) ( V11() real V116() ) Real)
for p being ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) st p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) = |[x : ( ( ) ( V11() real V116() ) Real) ,y : ( ( ) ( V11() real V116() ) Real) ,z : ( ( ) ( V11() real V116() ) Real) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) holds
( p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `1 : ( ( ) ( V11() real V116() ) Real) = x : ( ( ) ( V11() real V116() ) Real) & p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `2 : ( ( ) ( V11() real V116() ) Real) = y : ( ( ) ( V11() real V116() ) Real) & p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `3 : ( ( ) ( V11() real V116() ) Real) = z : ( ( ) ( V11() real V116() ) Real) ) ;

theorem :: EUCLID_5:15
for x1, y1, z1, x2, y2, z2 being ( ( ) ( V11() real V116() ) Real) holds |[x1 : ( ( ) ( V11() real V116() ) Real) ,y1 : ( ( ) ( V11() real V116() ) Real) ,z1 : ( ( ) ( V11() real V116() ) Real) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) <X> |[x2 : ( ( ) ( V11() real V116() ) Real) ,y2 : ( ( ) ( V11() real V116() ) Real) ,z2 : ( ( ) ( V11() real V116() ) Real) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) = |[((y1 : ( ( ) ( V11() real V116() ) Real) * z2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) - (z1 : ( ( ) ( V11() real V116() ) Real) * y2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,((z1 : ( ( ) ( V11() real V116() ) Real) * x2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) - (x1 : ( ( ) ( V11() real V116() ) Real) * z2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,((x1 : ( ( ) ( V11() real V116() ) Real) * y2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) - (y1 : ( ( ) ( V11() real V116() ) Real) * x2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ;

theorem :: EUCLID_5:16
for x being ( ( ) ( V11() real V116() ) Real)
for p1, p2 being ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) holds
( (x : ( ( ) ( V11() real V116() ) Real) * p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) <X> p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) = x : ( ( ) ( V11() real V116() ) Real) * (p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) <X> p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) & (x : ( ( ) ( V11() real V116() ) Real) * p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) <X> p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) = p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) <X> (x : ( ( ) ( V11() real V116() ) Real) * p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) ;

theorem :: EUCLID_5:17
for p1, p2 being ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) holds p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) <X> p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) = - (p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) <X> p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) ;

theorem :: EUCLID_5:18
for p1, p2 being ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) holds (- p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) <X> p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) = p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) <X> (- p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ;

theorem :: EUCLID_5:19
for x, y, z being ( ( ) ( V11() real V116() ) Real) holds |[0 : ( ( ) ( natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ,0 : ( ( ) ( natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ,0 : ( ( ) ( natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) <X> |[x : ( ( ) ( V11() real V116() ) Real) ,y : ( ( ) ( V11() real V116() ) Real) ,z : ( ( ) ( V11() real V116() ) Real) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) = 0. (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) ;

theorem :: EUCLID_5:20
for x1, x2 being ( ( ) ( V11() real V116() ) Real) holds |[x1 : ( ( ) ( V11() real V116() ) Real) ,0 : ( ( ) ( natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ,0 : ( ( ) ( natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) <X> |[x2 : ( ( ) ( V11() real V116() ) Real) ,0 : ( ( ) ( natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ,0 : ( ( ) ( natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) = 0. (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) ;

theorem :: EUCLID_5:21
for y1, y2 being ( ( ) ( V11() real V116() ) Real) holds |[0 : ( ( ) ( natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ,y1 : ( ( ) ( V11() real V116() ) Real) ,0 : ( ( ) ( natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) <X> |[0 : ( ( ) ( natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ,y2 : ( ( ) ( V11() real V116() ) Real) ,0 : ( ( ) ( natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) = 0. (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) ;

theorem :: EUCLID_5:22
for z1, z2 being ( ( ) ( V11() real V116() ) Real) holds |[0 : ( ( ) ( natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ,0 : ( ( ) ( natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ,z1 : ( ( ) ( V11() real V116() ) Real) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) <X> |[0 : ( ( ) ( natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ,0 : ( ( ) ( natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ,z2 : ( ( ) ( V11() real V116() ) Real) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) = 0. (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) ;

theorem :: EUCLID_5:23
for p1, p2, p3 being ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) holds p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) <X> (p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) + p3 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) = (p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) <X> p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) + (p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) <X> p3 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) ;

theorem :: EUCLID_5:24
for p1, p2, p3 being ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) holds (p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) + p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) <X> p3 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) = (p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) <X> p3 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) + (p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) <X> p3 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) ;

theorem :: EUCLID_5:25
for p1 being ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) holds p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) <X> p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) = 0. (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) ;

theorem :: EUCLID_5:26
for p1, p2, p3, p4 being ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) holds (p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) + p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) <X> (p3 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) + p4 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) = (((p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) <X> p3 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) + (p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) <X> p4 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) + (p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) <X> p3 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) + (p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) <X> p4 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) ;

theorem :: EUCLID_5:27
for p being ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) holds p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) = <*(p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `1) : ( ( ) ( V11() real V116() ) Real) ,(p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `2) : ( ( ) ( V11() real V116() ) Real) ,(p : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `3) : ( ( ) ( V11() real V116() ) Real) *> : ( ( ) ( V13() V16( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) Function-like FinSequence-like complex-yielding V120() V121() ) FinSequence of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ;

theorem :: EUCLID_5:28
for f1, f2 being ( ( ) ( V13() V16( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) Function-like FinSequence-like complex-yielding V120() V121() ) FinSequence of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) st len f1 : ( ( ) ( V13() V16( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) Function-like FinSequence-like complex-yielding V120() V121() ) FinSequence of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) = 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) & len f2 : ( ( ) ( V13() V16( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) Function-like FinSequence-like complex-yielding V120() V121() ) FinSequence of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) = 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) holds
mlt (f1 : ( ( ) ( V13() V16( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) Function-like FinSequence-like complex-yielding V120() V121() ) FinSequence of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,f2 : ( ( ) ( V13() V16( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) Function-like FinSequence-like complex-yielding V120() V121() ) FinSequence of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ) : ( ( ) ( V13() V16( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) Function-like FinSequence-like complex-yielding V120() V121() ) FinSequence of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) = <*((f1 : ( ( ) ( V13() V16( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) Function-like FinSequence-like complex-yielding V120() V121() ) FinSequence of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) . 1 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) * (f2 : ( ( ) ( V13() V16( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) Function-like FinSequence-like complex-yielding V120() V121() ) FinSequence of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) . 1 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,((f1 : ( ( ) ( V13() V16( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) Function-like FinSequence-like complex-yielding V120() V121() ) FinSequence of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) . 2 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) * (f2 : ( ( ) ( V13() V16( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) Function-like FinSequence-like complex-yielding V120() V121() ) FinSequence of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) . 2 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ,((f1 : ( ( ) ( V13() V16( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) Function-like FinSequence-like complex-yielding V120() V121() ) FinSequence of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) . 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) * (f2 : ( ( ) ( V13() V16( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) Function-like FinSequence-like complex-yielding V120() V121() ) FinSequence of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) . 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) *> : ( ( ) ( V13() V16( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) V17( REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) Function-like FinSequence-like complex-yielding V120() V121() ) FinSequence of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ;

theorem :: EUCLID_5:29
for p1, p2 being ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) holds |(p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ,p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) = (((p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `1) : ( ( ) ( V11() real V116() ) Real) * (p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `1) : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) + ((p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `2) : ( ( ) ( V11() real V116() ) Real) * (p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `2) : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) + ((p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `3) : ( ( ) ( V11() real V116() ) Real) * (p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) `3) : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ;

theorem :: EUCLID_5:30
for x3, y3 being ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) )
for x1, x2, y1, y2 being ( ( ) ( V11() real V116() ) Real) holds |(|[x1 : ( ( ) ( V11() real V116() ) Real) ,x2 : ( ( ) ( V11() real V116() ) Real) ,x3 : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ,|[y1 : ( ( ) ( V11() real V116() ) Real) ,y2 : ( ( ) ( V11() real V116() ) Real) ,y3 : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ]| : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) = ((x1 : ( ( ) ( V11() real V116() ) Real) * y1 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) + (x2 : ( ( ) ( V11() real V116() ) Real) * y2 : ( ( ) ( V11() real V116() ) Real) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) + (x3 : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) * y3 : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ;

definition
let p1, p2, p3 be ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ;
func |{p1,p2,p3}| -> ( ( real ) ( V11() real V116() ) number ) equals :: EUCLID_5:def 5
|(p1 : ( ( ) ( ) 2-sorted ) ,(p2 : ( ( ) ( ) set ) <X> p3 : ( ( ) ( ) Element of p1 : ( ( ) ( ) 2-sorted ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ;
end;

theorem :: EUCLID_5:31
for p1, p2 being ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) holds
( |{p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ,p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ,p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) }| : ( ( real ) ( V11() real V116() ) number ) = 0 : ( ( ) ( natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) & |{p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ,p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ,p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) }| : ( ( real ) ( V11() real V116() ) number ) = 0 : ( ( ) ( natural V11() real V30() V31() V116() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: EUCLID_5:32
for p1, p2, p3 being ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) holds p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) <X> (p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) <X> p3 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) = (|(p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ,p3 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) * p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) - (|(p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ,p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) * p3 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V198() ) ( V47() V73() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) ) ;

theorem :: EUCLID_5:33
for p1, p2, p3 being ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) holds |{p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ,p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ,p3 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) }| : ( ( real ) ( V11() real V116() ) number ) = |{p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ,p3 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ,p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) }| : ( ( real ) ( V11() real V116() ) number ) ;

theorem :: EUCLID_5:34
for p1, p2, p3 being ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) holds |{p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ,p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ,p3 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) }| : ( ( real ) ( V11() real V116() ) number ) = |{p3 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ,p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ,p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) }| : ( ( real ) ( V11() real V116() ) number ) ;

theorem :: EUCLID_5:35
for p1, p2, p3 being ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) holds |{p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ,p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ,p3 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) }| : ( ( real ) ( V11() real V116() ) number ) = |((p1 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) <X> p2 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) ,p3 : ( ( ) ( V13() Function-like V41(3 : ( ( ) ( V1() natural V11() real V30() V31() V116() V117() V129() V130() V131() V132() V133() V134() ) Element of NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) Element of K6(REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like complex-yielding V120() V121() ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real V116() ) Element of REAL : ( ( ) ( V1() V34() V129() V130() V131() V135() ) set ) ) ;