:: by Roland Coghetto and Adam Grabowski

::

:: Received March 11, 2019

:: Copyright (c) 2019-2021 Association of Mizar Users

definition

let S be non empty satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct ;

let a, b be POINT of S;

:: original: Line

redefine func Line (a,b) -> M3(K16( the U1 of S));

commutativity

for a, b being POINT of S holds Line (a,b) = Line (b,a) by GTARSKI3:83;

end;
let a, b be POINT of S;

:: original: Line

redefine func Line (a,b) -> M3(K16( the U1 of S));

commutativity

for a, b being POINT of S holds Line (a,b) = Line (b,a) by GTARSKI3:83;

LemmaA1: for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for a, b, c being POINT of S st Collinear a,b,c holds

c in Line (a,b)

proof end;

LemmaA2: for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for a, x, p being POINT of S st x in Line (a,p) holds

Collinear x,a,p

proof end;

theorem Prelim01: :: GTARSKI4:1

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity TarskiGeometryStruct

for a, b, c, d being POINT of S st a,b equiv c,d holds

( a,b equiv d,c & b,a equiv c,d & b,a equiv d,c & c,d equiv a,b & d,c equiv a,b & c,d equiv b,a & d,c equiv b,a )

for a, b, c, d being POINT of S st a,b equiv c,d holds

( a,b equiv d,c & b,a equiv c,d & b,a equiv d,c & c,d equiv a,b & d,c equiv a,b & c,d equiv b,a & d,c equiv b,a )

proof end;

theorem Prelim02: :: GTARSKI4:2

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity TarskiGeometryStruct

for p, q, a, b, c, d being POINT of S st ( p,q equiv a,b or p,q equiv b,a or q,p equiv a,b or q,p equiv b,a ) & ( p,q equiv c,d or p,q equiv d,c or q,p equiv c,d or q,p equiv d,c ) holds

( a,b equiv d,c & b,a equiv c,d & b,a equiv d,c & c,d equiv a,b & d,c equiv a,b & c,d equiv b,a & d,c equiv b,a )

for p, q, a, b, c, d being POINT of S st ( p,q equiv a,b or p,q equiv b,a or q,p equiv a,b or q,p equiv b,a ) & ( p,q equiv c,d or p,q equiv d,c or q,p equiv c,d or q,p equiv d,c ) holds

( a,b equiv d,c & b,a equiv c,d & b,a equiv d,c & c,d equiv a,b & d,c equiv a,b & c,d equiv b,a & d,c equiv b,a )

proof end;

theorem Prelim03: :: GTARSKI4:3

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity TarskiGeometryStruct

for p, q, a, b, c, d being POINT of S st ( p,q equiv a,b or p,q equiv b,a or q,p equiv a,b or q,p equiv b,a or a,b equiv p,q or b,a equiv p,q or a,b equiv q,p or b,a equiv q,p ) & ( p,q equiv c,d or p,q equiv d,c or q,p equiv c,d or q,p equiv d,c or c,d equiv p,q or d,c equiv p,q or c,d equiv q,p or d,c equiv q,p ) holds

( a,b equiv d,c & b,a equiv c,d & b,a equiv d,c & c,d equiv a,b & d,c equiv a,b & c,d equiv b,a & d,c equiv b,a & a,b equiv c,d )

for p, q, a, b, c, d being POINT of S st ( p,q equiv a,b or p,q equiv b,a or q,p equiv a,b or q,p equiv b,a or a,b equiv p,q or b,a equiv p,q or a,b equiv q,p or b,a equiv q,p ) & ( p,q equiv c,d or p,q equiv d,c or q,p equiv c,d or q,p equiv d,c or c,d equiv p,q or d,c equiv p,q or c,d equiv q,p or d,c equiv q,p ) holds

( a,b equiv d,c & b,a equiv c,d & b,a equiv d,c & c,d equiv a,b & d,c equiv a,b & c,d equiv b,a & d,c equiv b,a & a,b equiv c,d )

proof end;

theorem Prelim05: :: GTARSKI4:4

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct

for a, b being POINT of S holds

( Collinear a,b,b & Collinear b,b,a & Collinear b,a,b )

for a, b being POINT of S holds

( Collinear a,b,b & Collinear b,b,a & Collinear b,a,b )

proof end;

theorem Prelim07: :: GTARSKI4:5

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for p, q, r being POINT of S st p <> q & p <> r & ( Collinear p,q,r or Collinear q,r,p or Collinear r,p,q or Collinear p,r,q or Collinear q,p,r or Collinear r,q,p ) holds

( Line (p,q) = Line (p,r) & Line (p,q) = Line (r,p) & Line (q,p) = Line (p,r) & Line (q,p) = Line (r,p) )

for p, q, r being POINT of S st p <> q & p <> r & ( Collinear p,q,r or Collinear q,r,p or Collinear r,p,q or Collinear p,r,q or Collinear q,p,r or Collinear r,q,p ) holds

( Line (p,q) = Line (p,r) & Line (p,q) = Line (r,p) & Line (q,p) = Line (p,r) & Line (q,p) = Line (r,p) )

proof end;

theorem Prelim08: :: GTARSKI4:6

for S being TarskiGeometryStruct

for a, b, c being POINT of S st ( Middle a,b,c or between a,b,c ) holds

Collinear a,b,c

for a, b, c being POINT of S st ( Middle a,b,c or between a,b,c ) holds

Collinear a,b,c

proof end;

theorem Prelim08a: :: GTARSKI4:7

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct

for a, b, c being POINT of S st ( Middle a,b,c or between a,b,c ) holds

( Collinear a,b,c & Collinear b,c,a & Collinear c,a,b & Collinear c,b,a & Collinear b,a,c & Collinear a,c,b )

for a, b, c being POINT of S st ( Middle a,b,c or between a,b,c ) holds

( Collinear a,b,c & Collinear b,c,a & Collinear c,a,b & Collinear c,b,a & Collinear b,a,c & Collinear a,c,b )

proof end;

theorem Prelim08b: :: GTARSKI4:8

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d being POINT of S st a <> b & Collinear a,b,c & Collinear a,b,d holds

Collinear a,c,d

for a, b, c, d being POINT of S st a <> b & Collinear a,b,c & Collinear a,b,d holds

Collinear a,c,d

proof end;

theorem Prelim09: :: GTARSKI4:9

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for a, b being POINT of S st ( Middle a,a,b or Middle a,b,b or Middle a,b,a ) holds

a = b

for a, b being POINT of S st ( Middle a,a,b or Middle a,b,b or Middle a,b,a ) holds

a = b

proof end;

theorem Prelim10: :: GTARSKI4:10

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for a, b, c being POINT of S st ( Middle a,b,c or Middle c,b,a ) & ( a <> b or b <> c ) holds

( Line (b,a) = Line (b,c) & Line (a,b) = Line (b,c) & Line (a,b) = Line (c,b) & Line (b,a) = Line (c,b) )

for a, b, c being POINT of S st ( Middle a,b,c or Middle c,b,a ) & ( a <> b or b <> c ) holds

( Line (b,a) = Line (b,c) & Line (a,b) = Line (b,c) & Line (a,b) = Line (c,b) & Line (b,a) = Line (c,b) )

proof end;

theorem Prelim11: :: GTARSKI4:11

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, c9 being POINT of S st a <> b & c <> c9 & ( c in Line (a,b) or c in Line (b,a) ) & ( c9 in Line (a,b) or c9 in Line (b,a) ) holds

( Line (c,c9) = Line (a,b) & Line (c,c9) = Line (b,a) & Line (c9,c) = Line (b,a) & Line (c9,c) = Line (a,b) )

for a, b, c, c9 being POINT of S st a <> b & c <> c9 & ( c in Line (a,b) or c in Line (b,a) ) & ( c9 in Line (a,b) or c9 in Line (b,a) ) holds

( Line (c,c9) = Line (a,b) & Line (c,c9) = Line (b,a) & Line (c9,c) = Line (b,a) & Line (c9,c) = Line (a,b) )

proof end;

theorem Prelim12: :: GTARSKI4:12

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for b, c, p being POINT of S holds Middle reflection (p,c), reflection (p,b), reflection (p,(reflection (b,c)))

for b, c, p being POINT of S holds Middle reflection (p,c), reflection (p,b), reflection (p,(reflection (b,c)))

proof end;

definition

let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity TarskiGeometryStruct ;

let a, b, c be POINT of S;

end;
let a, b, c be POINT of S;

:: deftheorem defines right_angle GTARSKI4:def 1 :

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity TarskiGeometryStruct

for a, b, c being POINT of S holds

( right_angle a,b,c iff a,c equiv a, reflection (b,c) );

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity TarskiGeometryStruct

for a, b, c being POINT of S holds

( right_angle a,b,c iff a,c equiv a, reflection (b,c) );

:: 8.2 Satz

theorem Satz8p2: :: GTARSKI4:13

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c being POINT of S st right_angle a,b,c holds

right_angle c,b,a

for a, b, c being POINT of S st right_angle a,b,c holds

right_angle c,b,a

proof end;

theorem Lem01: :: GTARSKI4:14

for S being satisfying_Tarski-model TarskiGeometryStruct

for a being POINT of S holds reflection (a,a) = a

for a being POINT of S holds reflection (a,a) = a

proof end;

:: 8.3 Satz

theorem Satz8p3: :: GTARSKI4:15

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, a9, b, c being POINT of S st right_angle a,b,c & a <> b & Collinear b,a,a9 holds

right_angle a9,b,c

for a, a9, b, c being POINT of S st right_angle a,b,c & a <> b & Collinear b,a,a9 holds

right_angle a9,b,c

proof end;

theorem :: GTARSKI4:16

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c being POINT of S st right_angle a,b,c holds

right_angle a,b, reflection (b,c)

for a, b, c being POINT of S st right_angle a,b,c holds

right_angle a,b, reflection (b,c)

proof end;

:: 8.5 Satz

theorem Satz8p5: :: GTARSKI4:17

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b being POINT of S holds right_angle a,b,b

for a, b being POINT of S holds right_angle a,b,b

proof end;

:: 8.6 Satz

theorem Satz8p6: :: GTARSKI4:18

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, a9, b, c being POINT of S st right_angle a,b,c & right_angle a9,b,c & between a,c,a9 holds

b = c

for a, a9, b, c being POINT of S st right_angle a,b,c & right_angle a9,b,c & between a,c,a9 holds

b = c

proof end;

:: 8.7 Satz

theorem Satz8p7: :: GTARSKI4:19

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c being POINT of S st right_angle a,b,c & right_angle a,c,b holds

b = c

for a, b, c being POINT of S st right_angle a,b,c & right_angle a,c,b holds

b = c

proof end;

:: 8.8 Satz

theorem Satz8p8: :: GTARSKI4:20

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b being POINT of S st right_angle a,b,a holds

a = b

for a, b being POINT of S st right_angle a,b,a holds

a = b

proof end;

:: 8.9 Satz

theorem Satz8p9: :: GTARSKI4:21

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c being POINT of S st right_angle a,b,c & Collinear a,b,c & not a = b holds

c = b

for a, b, c being POINT of S st right_angle a,b,c & Collinear a,b,c & not a = b holds

c = b

proof end;

:: 8.10 Satz

theorem Satz8p10: :: GTARSKI4:22

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, a9, b, b9, c, c9 being POINT of S st right_angle a,b,c & a,b,c cong a9,b9,c9 holds

right_angle a9,b9,c9

for a, a9, b, b9, c, c9 being POINT of S st right_angle a,b,c & a,b,c cong a9,b9,c9 holds

right_angle a9,b9,c9

proof end;

definition

let S be non empty satisfying_Tarski-model TarskiGeometryStruct ;

let A, A9 be Subset of S;

let x be POINT of S;

end;
let A, A9 be Subset of S;

let x be POINT of S;

pred are_orthogonal A,x,A9 means :: GTARSKI4:def 2

( A is_line & A9 is_line & x in A & x in A9 & ( for u, v being POINT of S st u in A & v in A9 holds

right_angle u,x,v ) );

( A is_line & A9 is_line & x in A & x in A9 & ( for u, v being POINT of S st u in A & v in A9 holds

right_angle u,x,v ) );

:: deftheorem defines are_orthogonal GTARSKI4:def 2 :

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for A, A9 being Subset of S

for x being POINT of S holds

( are_orthogonal A,x,A9 iff ( A is_line & A9 is_line & x in A & x in A9 & ( for u, v being POINT of S st u in A & v in A9 holds

right_angle u,x,v ) ) );

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for A, A9 being Subset of S

for x being POINT of S holds

( are_orthogonal A,x,A9 iff ( A is_line & A9 is_line & x in A & x in A9 & ( for u, v being POINT of S st u in A & v in A9 holds

right_angle u,x,v ) ) );

definition
end;

:: deftheorem defines are_orthogonal GTARSKI4:def 3 :

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for A, A9 being Subset of S holds

( are_orthogonal A,A9 iff ex x being POINT of S st are_orthogonal A,x,A9 );

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for A, A9 being Subset of S holds

( are_orthogonal A,A9 iff ex x being POINT of S st are_orthogonal A,x,A9 );

definition

let S be non empty satisfying_Tarski-model TarskiGeometryStruct ;

let A be Subset of S;

let x, c, d be POINT of S;

end;
let A be Subset of S;

let x, c, d be POINT of S;

:: deftheorem defines are_lorthogonal GTARSKI4:def 4 :

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for A being Subset of S

for x, c, d being POINT of S holds

( are_lorthogonal A,x,c,d iff ( c <> d & are_orthogonal A,x, Line (c,d) ) );

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for A being Subset of S

for x, c, d being POINT of S holds

( are_lorthogonal A,x,c,d iff ( c <> d & are_orthogonal A,x, Line (c,d) ) );

definition

let S be non empty satisfying_Tarski-model TarskiGeometryStruct ;

let a, b, x, c, d be POINT of S;

end;
let a, b, x, c, d be POINT of S;

pred are_orthogonal a,b,x,c,d means :: GTARSKI4:def 5

( a <> b & c <> d & are_orthogonal Line (a,b),x, Line (c,d) );

( a <> b & c <> d & are_orthogonal Line (a,b),x, Line (c,d) );

:: deftheorem defines are_orthogonal GTARSKI4:def 5 :

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for a, b, x, c, d being POINT of S holds

( are_orthogonal a,b,x,c,d iff ( a <> b & c <> d & are_orthogonal Line (a,b),x, Line (c,d) ) );

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for a, b, x, c, d being POINT of S holds

( are_orthogonal a,b,x,c,d iff ( a <> b & c <> d & are_orthogonal Line (a,b),x, Line (c,d) ) );

definition

let S be non empty satisfying_Tarski-model TarskiGeometryStruct ;

let a, b, c, d be POINT of S;

end;
let a, b, c, d be POINT of S;

pred are_orthogonal a,b,c,d means :: GTARSKI4:def 6

( a <> b & c <> d & are_orthogonal Line (a,b), Line (c,d) );

( a <> b & c <> d & are_orthogonal Line (a,b), Line (c,d) );

:: deftheorem defines are_orthogonal GTARSKI4:def 6 :

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d being POINT of S holds

( are_orthogonal a,b,c,d iff ( a <> b & c <> d & are_orthogonal Line (a,b), Line (c,d) ) );

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d being POINT of S holds

( are_orthogonal a,b,c,d iff ( a <> b & c <> d & are_orthogonal Line (a,b), Line (c,d) ) );

:: 8.12 Satz

theorem Satz8p12: :: GTARSKI4:23

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for A, A9 being Subset of S

for x being POINT of S holds

( are_orthogonal A,x,A9 iff are_orthogonal A9,x,A ) by Satz8p2;

for A, A9 being Subset of S

for x being POINT of S holds

( are_orthogonal A,x,A9 iff are_orthogonal A9,x,A ) by Satz8p2;

:: 8.13 Satz

theorem Satz8p13: :: GTARSKI4:24

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for A, A9 being Subset of S

for x being POINT of S holds

( are_orthogonal A,x,A9 iff ( A is_line & A9 is_line & x in A & x in A9 & ex u, v being POINT of S st

( u in A & v in A9 & u <> x & v <> x & right_angle u,x,v ) ) )

for A, A9 being Subset of S

for x being POINT of S holds

( are_orthogonal A,x,A9 iff ( A is_line & A9 is_line & x in A & x in A9 & ex u, v being POINT of S st

( u in A & v in A9 & u <> x & v <> x & right_angle u,x,v ) ) )

proof end;

theorem Satz8p14p1: :: GTARSKI4:25

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for A, A9 being Subset of S st are_orthogonal A,A9 holds

A <> A9

for A, A9 being Subset of S st are_orthogonal A,A9 holds

A <> A9

proof end;

:: 6.22 Satz

definition
end;

:: deftheorem defines Is GTARSKI4:def 7 :

for S being non empty TarskiGeometryStruct

for A, B being Subset of S

for x being POINT of S holds

( A,B Is x iff ( A is_line & B is_line & A <> B & x in A & x in B ) );

for S being non empty TarskiGeometryStruct

for A, B being Subset of S

for x being POINT of S holds

( A,B Is x iff ( A is_line & B is_line & A <> B & x in A & x in B ) );

theorem Satz8p14p2: :: GTARSKI4:26

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for A, A9 being Subset of S

for x being POINT of S holds

( are_orthogonal A,x,A9 iff ( are_orthogonal A,A9 & A,A9 Is x ) )

for A, A9 being Subset of S

for x being POINT of S holds

( are_orthogonal A,x,A9 iff ( are_orthogonal A,A9 & A,A9 Is x ) )

proof end;

theorem :: GTARSKI4:27

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for A, A9 being Subset of S

for x, y being POINT of S st are_orthogonal A,x,A9 & are_orthogonal A,y,A9 holds

x = y

for A, A9 being Subset of S

for x, y being POINT of S st are_orthogonal A,x,A9 & are_orthogonal A,y,A9 holds

x = y

proof end;

theorem Satz8p15a: :: GTARSKI4:28

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for x, a, b, c being POINT of S st Collinear a,b,x & are_orthogonal a,b,c,x holds

are_orthogonal a,b,x,c,x

for x, a, b, c being POINT of S st Collinear a,b,x & are_orthogonal a,b,c,x holds

are_orthogonal a,b,x,c,x

proof end;

:: 8.15 Satz

theorem Satz8p15: :: GTARSKI4:29

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for x, a, b, c being POINT of S st a <> b & Collinear a,b,x holds

( are_orthogonal a,b,c,x iff are_orthogonal a,b,x,c,x )

for x, a, b, c being POINT of S st a <> b & Collinear a,b,x holds

( are_orthogonal a,b,c,x iff are_orthogonal a,b,x,c,x )

proof end;

:: 8.16 Satz

theorem :: GTARSKI4:30

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for x, a, b, c, u being POINT of S st a <> b & Collinear a,b,x & Collinear a,b,u & u <> x holds

( are_orthogonal a,b,c,x iff ( not Collinear a,b,c & right_angle c,x,u ) )

for x, a, b, c, u being POINT of S st a <> b & Collinear a,b,x & Collinear a,b,u & u <> x holds

( are_orthogonal a,b,c,x iff ( not Collinear a,b,c & right_angle c,x,u ) )

proof end;

definition
end;

:: deftheorem defines is_foot GTARSKI4:def 8 :

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, x being POINT of S holds

( x is_foot a,b,c iff ( Collinear a,b,x & are_orthogonal a,b,c,x ) );

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, x being POINT of S holds

( x is_foot a,b,c iff ( Collinear a,b,x & are_orthogonal a,b,c,x ) );

theorem Satz8p18Uniqueness: :: GTARSKI4:31

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for x, y, a, b, c being POINT of S st x is_foot a,b,c & y is_foot a,b,c holds

x = y

for x, y, a, b, c being POINT of S st x is_foot a,b,c & y is_foot a,b,c holds

x = y

proof end;

theorem Satz8p18Lemma: :: GTARSKI4:32

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for x, y, z, a, b, c, c9, p, q, q9 being POINT of S st not Collinear a,b,c & between b,a,y & a <> y & between a,y,z & y,z equiv y,p & y <> p & q9 = reflection (z,q) & Middle c,x,c9 & c <> y & between q9,y,c9 & Middle y,p,c & between p,y,q & q <> q9 holds

x <> y

for x, y, z, a, b, c, c9, p, q, q9 being POINT of S st not Collinear a,b,c & between b,a,y & a <> y & between a,y,z & y,z equiv y,p & y <> p & q9 = reflection (z,q) & Middle c,x,c9 & c <> y & between q9,y,c9 & Middle y,p,c & between p,y,q & q <> q9 holds

x <> y

proof end;

theorem Satz8p18pExistence: :: GTARSKI4:33

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a, b, c being POINT of S st not Collinear a,b,c holds

ex x being POINT of S st x is_foot a,b,c

for a, b, c being POINT of S st not Collinear a,b,c holds

ex x being POINT of S st x is_foot a,b,c

proof end;

:: 8.20 Lemma

theorem Lemma8p20: :: GTARSKI4:34

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a, b, c, p being POINT of S st right_angle a,b,c & Middle reflection (a,c),p, reflection (b,c) holds

( right_angle b,a,p & ( b <> c implies a <> p ) )

for a, b, c, p being POINT of S st right_angle a,b,c & Middle reflection (a,c),p, reflection (b,c) holds

( right_angle b,a,p & ( b <> c implies a <> p ) )

proof end;

theorem Satz8p21p1: :: GTARSKI4:35

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a, b, c being POINT of S st not Collinear a,b,c holds

ex p, t being POINT of S st

( are_orthogonal a,b,p,a & Collinear a,b,t & between c,t,p )

for a, b, c being POINT of S st not Collinear a,b,c holds

ex p, t being POINT of S st

( are_orthogonal a,b,p,a & Collinear a,b,t & between c,t,p )

proof end;

:: 8.21 Satz

theorem Satz8p21: :: GTARSKI4:36

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a, b, c being POINT of S st a <> b holds

ex p, t being POINT of S st

( are_orthogonal a,b,p,a & Collinear a,b,t & between c,t,p )

for a, b, c being POINT of S st a <> b holds

ex p, t being POINT of S st

( are_orthogonal a,b,p,a & Collinear a,b,t & between c,t,p )

proof end;

theorem Th01: :: GTARSKI4:37

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a, b, p, q being POINT of S st a <> b & a <> p & right_angle b,a,p & right_angle a,b,q holds

not Collinear p,a,q

for a, b, p, q being POINT of S st a <> b & a <> p & right_angle b,a,p & right_angle a,b,q holds

not Collinear p,a,q

proof end;

LemmaA3: for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a, b, p being POINT of S st a <> p holds

reflection (a,p) <> p

proof end;

theorem Satz8p22lemma: :: GTARSKI4:38

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a, b, p, q, t being POINT of S st a,p <= b,q & are_orthogonal a,b,q,b & are_orthogonal a,b,p,a & Collinear a,b,t & between q,t,p holds

ex x being POINT of S st Middle a,x,b

for a, b, p, q, t being POINT of S st a,p <= b,q & are_orthogonal a,b,q,b & are_orthogonal a,b,p,a & Collinear a,b,t & between q,t,p holds

ex x being POINT of S st Middle a,x,b

proof end;

:: 8.22 Satz

theorem Satz8p22: :: GTARSKI4:39

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a, b being POINT of S ex x being POINT of S st Middle a,x,b

for a, b being POINT of S ex x being POINT of S st Middle a,x,b

proof end;

definition

let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ;

let a, b be POINT of S;

existence

ex b_{1} being POINT of S st Middle a,b_{1},b
by Satz8p22;

uniqueness

for b_{1}, b_{2} being POINT of S st Middle a,b_{1},b & Middle a,b_{2},b holds

b_{1} = b_{2}
by GTARSKI3:108;

end;
let a, b be POINT of S;

existence

ex b

uniqueness

for b

b

:: deftheorem defines Midpoint GTARSKI4:def 9 :

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a, b, b_{4} being POINT of S holds

( b_{4} = Midpoint (a,b) iff Middle a,b_{4},b );

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a, b, b

( b

:: 8.24 Lemma

theorem :: GTARSKI4:40

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a, b, p, q, r, t being POINT of S st are_orthogonal p,a,a,b & are_orthogonal q,b,a,b & Collinear a,b,t & between p,t,q & between b,r,q & a,p equiv b,r holds

ex x being POINT of S st

( Middle a,x,b & Middle p,x,r )

for a, b, p, q, r, t being POINT of S st are_orthogonal p,a,a,b & are_orthogonal q,b,a,b & Collinear a,b,t & between p,t,q & between b,r,q & a,p equiv b,r holds

ex x being POINT of S st

( Middle a,x,b & Middle p,x,r )

proof end;

theorem :: GTARSKI4:41

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a, b, c, d, x, p, q being POINT of S st c in Line (a,b) & d in Line (a,b) & a <> b & c <> d holds

Line (a,b) = Line (c,d) by Prelim11;

for a, b, c, d, x, p, q being POINT of S st c in Line (a,b) & d in Line (a,b) & a <> b & c <> d holds

Line (a,b) = Line (c,d) by Prelim11;

theorem :: GTARSKI4:42

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a, b, c, d, x, p, q being POINT of S st c in Line (a,b) & d in Line (a,b) & c <> d & are_orthogonal a,b,x,p,q holds

are_orthogonal c,d,x,p,q by Prelim11;

for a, b, c, d, x, p, q being POINT of S st c in Line (a,b) & d in Line (a,b) & c <> d & are_orthogonal a,b,x,p,q holds

are_orthogonal c,d,x,p,q by Prelim11;

theorem :: GTARSKI4:43

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a, b, c, d, p, q being POINT of S st p in Line (a,b) & q in Line (a,b) & a <> b & are_orthogonal p,q,c,d holds

are_orthogonal a,b,c,d by Prelim11;

for a, b, c, d, p, q being POINT of S st p in Line (a,b) & q in Line (a,b) & a <> b & are_orthogonal p,q,c,d holds

are_orthogonal a,b,c,d by Prelim11;

theorem :: GTARSKI4:44

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a, b, c, d being POINT of S st a <> b & b <> c & c <> d & a <> c & a <> d & b <> d & are_orthogonal b,a,a,c & Collinear a,c,d holds

are_orthogonal b,a,a,d

for a, b, c, d being POINT of S st a <> b & b <> c & c <> d & a <> c & a <> d & b <> d & are_orthogonal b,a,a,c & Collinear a,c,d holds

are_orthogonal b,a,a,d

proof end;

theorem :: GTARSKI4:45

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a, b, p, q being POINT of S st are_orthogonal a,b,p,q holds

are_orthogonal a,b,q,p ;

for a, b, p, q being POINT of S st are_orthogonal a,b,p,q holds

are_orthogonal a,b,q,p ;

theorem ExtPerp5: :: GTARSKI4:46

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a, b, c, d, p, q being POINT of S st p in Line (a,b) & q in Line (a,b) & p <> q & are_orthogonal a,b,c,d holds

are_orthogonal p,q,c,d by Prelim11;

for a, b, c, d, p, q being POINT of S st p in Line (a,b) & q in Line (a,b) & p <> q & are_orthogonal a,b,c,d holds

are_orthogonal p,q,c,d by Prelim11;

theorem :: GTARSKI4:47

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a, b, c, d, p, q being POINT of S st Collinear a,b,p & Collinear a,b,q & p <> q & are_orthogonal a,b,c,d holds

are_orthogonal p,q,c,d

for a, b, c, d, p, q being POINT of S st Collinear a,b,p & Collinear a,b,q & p <> q & are_orthogonal a,b,c,d holds

are_orthogonal p,q,c,d

proof end;

theorem :: GTARSKI4:48

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a, b, c, d, p, q being POINT of S st p in Line (a,b) & q in Line (a,b) & p <> q & a <> b & are_orthogonal c,d,p,q holds

are_orthogonal c,d,a,b by Prelim11;

for a, b, c, d, p, q being POINT of S st p in Line (a,b) & q in Line (a,b) & p <> q & a <> b & are_orthogonal c,d,p,q holds

are_orthogonal c,d,a,b by Prelim11;