:: PARSP_2 semantic presentation

Lemma1: for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ st b₂ - b₃ = 0. b₁ holds
b₂ = b₃

proof end;

Lemma2: for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃ being Element of b₁ holds
( ( b₂ + (- b₃) = 0. b₁ implies b₂ = b₃ ) & ( b₂ = b₃ implies b₂ + (- b₃) = 0. b₁ ) & ( b₂ - b₃ = 0. b₁ implies b₂ = b₃ ) & ( b₂ = b₃ implies b₂ - b₃ = 0. b₁ ) )

proof end;

theorem Th1: :: PARSP_2:1

for b₁ being Field holds MPS b₁ is ParSp

proof end;

Lemma4: for b₁ being Field
for b₂, b₃, b₄, b₅ being Element of [:the carrier of b₁,the carrier of b₁,the carrier of b₁:] holds
( ( (((b₂ `1 ) - (b₃ `1 )) * ((b₄ `2 ) - (b₅ `2 ))) - (((b₄ `1 ) - (b₅ `1 )) * ((b₂ `2 ) - (b₃ `2 ))) = 0. b₁ & (((b₂ `1 ) - (b₃ `1 )) * ((b₄ `3 ) - (b₅ `3 ))) - (((b₄ `1 ) - (b₅ `1 )) * ((b₂ `3 ) - (b₃ `3 ))) = 0. b₁ & (((b₂ `2 ) - (b₃ `2 )) * ((b₄ `3 ) - (b₅ `3 ))) - (((b₄ `2 ) - (b₅ `2 )) * ((b₂ `3 ) - (b₃ `3 ))) = 0. b₁ ) iff ( ex b₆ being Element of b₁ st
( b₆ * ((b₂ `1 ) - (b₃ `1 )) = (b₄ `1 ) - (b₅ `1 ) & b₆ * ((b₂ `2 ) - (b₃ `2 )) = (b₄ `2 ) - (b₅ `2 ) & b₆ * ((b₂ `3 ) - (b₃ `3 )) = (b₄ `3 ) - (b₅ `3 ) ) or ( (b₂ `1 ) - (b₃ `1 ) = 0. b₁ & (b₂ `2 ) - (b₃ `2 ) = 0. b₁ & (b₂ `3 ) - (b₃ `3 ) = 0. b₁ ) ) )

proof end;

theorem Th2: :: PARSP_2:2

for b₁ being Field
for b₂, b₃, b₄, b₅ being Element of (MPS b₁) holds
( b₂,b₃ '||' b₄,b₅ iff ex b₆, b₇, b₈, b₉ being Element of [:the carrier of b₁,the carrier of b₁,the carrier of b₁:] st
( [b₂,b₃,b₄,b₅] = [b₆,b₇,b₈,b₉] & ( ex b₁₀ being Element of b₁ st
( b₁₀ * ((b₆ `1 ) - (b₇ `1 )) = (b₈ `1 ) - (b₉ `1 ) & b₁₀ * ((b₆ `2 ) - (b₇ `2 )) = (b₈ `2 ) - (b₉ `2 ) & b₁₀ * ((b₆ `3 ) - (b₇ `3 )) = (b₈ `3 ) - (b₉ `3 ) ) or ( (b₆ `1 ) - (b₇ `1 ) = 0. b₁ & (b₆ `2 ) - (b₇ `2 ) = 0. b₁ & (b₆ `3 ) - (b₇ `3 ) = 0. b₁ ) ) ) )

proof end;

theorem Th3: :: PARSP_2:3

for b₁ being Field
for b₂, b₃, b₄ being Element of (MPS b₁)
for b₅, b₆, b₇ being Element of [:the carrier of b₁,the carrier of b₁,the carrier of b₁:] st not b₂,b₃ '||' b₂,b₄ & [b₂,b₃,b₂,b₄] = [b₅,b₆,b₅,b₇] holds
( b₅ <> b₆ & b₅ <> b₇ & b₆ <> b₇ )

proof end;

theorem Th4: :: PARSP_2:4

for b₁ being Field
for b₂, b₃, b₄ being Element of (MPS b₁)
for b₅, b₆, b₇ being Element of [:the carrier of b₁,the carrier of b₁,the carrier of b₁:]
for b₈, b₉ being Element of b₁ st not b₂,b₃ '||' b₂,b₄ & [b₂,b₃,b₂,b₄] = [b₅,b₆,b₅,b₇] & b₈ * ((b₅ `1 ) - (b₆ `1 )) = b₉ * ((b₅ `1 ) - (b₇ `1 )) & b₈ * ((b₅ `2 ) - (b₆ `2 )) = b₉ * ((b₅ `2 ) - (b₇ `2 )) & b₈ * ((b₅ `3 ) - (b₆ `3 )) = b₉ * ((b₅ `3 ) - (b₇ `3 )) holds
( b₈ = 0. b₁ & b₉ = 0. b₁ )

proof end;

Lemma8: for b₁ being non empty add-associative right_zeroed right_complementable LoopStr
for b₂, b₃, b₄ being Element of b₁ holds (b₃ + b₂) - (b₄ + b₂) = b₃ - b₄

proof end;

Lemma9: for b₁ being Field
for b₂, b₃, b₄ being Element of b₁ holds (b₂ - b₃) - (b₄ - b₃) = b₂ - b₄

proof end;

Lemma10: for b₁ being Field
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st (b₂ * (b₃ - b₄)) - (b₅ * (b₃ - b₆)) = b₆ - b₄ holds
(b₂ + (- (1. b₁))) * (b₃ - b₄) = (b₅ + (- (1. b₁))) * (b₃ - b₆)

proof end;

Lemma11: for b₁ being Field
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ - b₃ = b₄ - b₅ holds
b₅ = (b₃ + b₄) - b₂

proof end;

theorem Th5: :: PARSP_2:5

for b₁ being Field
for b₂, b₃, b₄, b₅ being Element of (MPS b₁)
for b₆, b₇, b₈, b₉ being Element of [:the carrier of b₁,the carrier of b₁,the carrier of b₁:] st not b₂,b₃ '||' b₂,b₄ & b₂,b₃ '||' b₄,b₅ & b₂,b₄ '||' b₃,b₅ & [b₂,b₃,b₄,b₅] = [b₆,b₇,b₈,b₉] holds
( b₉ `1 = ((b₇ `1 ) + (b₈ `1 )) - (b₆ `1 ) & b₉ `2 = ((b₇ `2 ) + (b₈ `2 )) - (b₆ `2 ) & b₉ `3 = ((b₇ `3 ) + (b₈ `3 )) - (b₆ `3 ) )

proof end;

Lemma13: for b₁ being Field
for b₂, b₃, b₄ being Element of b₁ st (b₂ * b₃) - (b₂ * b₄) = b₄ + b₃ holds
(b₂ - (1. b₁)) * b₃ = (b₂ + (1. b₁)) * b₄

proof end;

Lemma14: for b₁ being Field
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st b₂ * (b₃ - b₄) = b₅ - b₆ & b₆ = (b₃ + b₄) - b₅ holds
(b₂ - (1. b₁)) * (b₅ - b₄) = (b₂ + (1. b₁)) * (b₅ - b₃)

proof end;

Lemma15: for b₁ being Field
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st b₂ = (b₃ + b₄) - b₅ & b₆ = (b₃ + b₇) - b₅ holds
(1. b₁) * (b₄ - b₇) = b₂ - b₆

proof end;

theorem Th6: :: PARSP_2:6

for b₁ being Field holds
not for b₂, b₃, b₄ being Element of (MPS b₁) holds b₂,b₃ '||' b₂,b₄

proof end;

theorem Th7: :: PARSP_2:7

for b₁ being Field
for b₂, b₃, b₄, b₅ being Element of (MPS b₁) st (1. b₁) + (1. b₁) <> 0. b₁ & b₂,b₃ '||' b₄,b₅ & b₄,b₂ '||' b₃,b₅ & b₄,b₃ '||' b₂,b₅ holds
b₄,b₂ '||' b₄,b₃

proof end;

theorem Th8: :: PARSP_2:8

for b₁ being Field
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of (MPS b₁) st not b₂,b₃ '||' b₂,b₄ & not b₂,b₃ '||' b₂,b₅ & b₂,b₃ '||' b₄,b₆ & b₂,b₃ '||' b₅,b₇ & b₂,b₄ '||' b₃,b₆ & b₂,b₅ '||' b₃,b₇ holds
b₄,b₅ '||' b₆,b₇

proof end;

definition

let c₁ be ParSp;
attr a₁ is FanodesSp-like means :Def1: :: PARSP_2:def 1
( not for b₁, b₂, b₃ being Element of a₁ holds b₁,b₂ '||' b₁,b₃ & ( for b₁, b₂, b₃, b₄ being Element of a₁ st b₂,b₃ '||' b₁,b₄ & b₁,b₂ '||' b₃,b₄ & b₁,b₃ '||' b₂,b₄ holds
b₁,b₂ '||' b₁,b₃ ) & ( for b₁, b₂, b₃, b₄, b₅, b₆ being Element of a₁ st not b₁,b₄ '||' b₁,b₂ & not b₁,b₄ '||' b₁,b₃ & b₁,b₄ '||' b₂,b₅ & b₁,b₄ '||' b₃,b₆ & b₁,b₂ '||' b₄,b₅ & b₁,b₃ '||' b₄,b₆ holds
b₂,b₃ '||' b₅,b₆ ) );

end;

:: deftheorem Def1 defines FanodesSp-like PARSP_2:def 1 :

registration

cluster strict FanodesSp-like ParStr ;
existence

proof end;

end;

definition

mode FanodesSp is FanodesSp-like ParSp;

end;

theorem Th9: :: PARSP_2:9

canceled;

theorem Th10: :: PARSP_2:10

canceled;

theorem Th11: :: PARSP_2:11

canceled;

theorem Th12: :: PARSP_2:12

canceled;

theorem Th13: :: PARSP_2:13

for b₁ being FanodesSp
for b₂, b₃ being Element of b₁ st b₂ <> b₃ holds
ex b₄ being Element of b₁ st not b₂,b₃ '||' b₂,b₄

proof end;

definition

let c₁ be FanodesSp;
let c₂, c₃, c₄ be Element of c₁;
pred c₂,c₃,c₄ is_collinear means :Def2: :: PARSP_2:def 2
a₂,a₃ '||' a₂,a₄;

end;

:: deftheorem Def2 defines is_collinear PARSP_2:def 2 :

theorem Th14: :: PARSP_2:14

canceled;

theorem Th15: :: PARSP_2:15

for b₁ being FanodesSp
for b₂, b₃, b₄ being Element of b₁ st b₂,b₃,b₄ is_collinear holds
( b₂,b₄,b₃ is_collinear & b₄,b₃,b₂ is_collinear & b₃,b₂,b₄ is_collinear & b₃,b₄,b₂ is_collinear & b₄,b₂,b₃ is_collinear )

proof end;

theorem Th16: :: PARSP_2:16

canceled;

theorem Th17: :: PARSP_2:17

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st not b₂,b₃,b₄ is_collinear & b₂,b₃ '||' b₅,b₆ & b₂,b₄ '||' b₅,b₇ & b₅ <> b₆ & b₅ <> b₇ holds
not b₅,b₆,b₇ is_collinear

proof end;

theorem Th18: :: PARSP_2:18

for b₁ being FanodesSp
for b₂, b₃, b₄ being Element of b₁ st ( b₂ = b₃ or b₃ = b₄ or b₄ = b₂ ) holds
b₂,b₃,b₄ is_collinear

proof end;

theorem Th19: :: PARSP_2:19

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st b₂ <> b₃ & b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear & b₂,b₃,b₆ is_collinear holds
b₄,b₅,b₆ is_collinear

proof end;

theorem Th20: :: PARSP_2:20

for b₁ being FanodesSp
for b₂, b₃ being Element of b₁ st b₂ <> b₃ holds
ex b₄ being Element of b₁ st not b₂,b₃,b₄ is_collinear

proof end;

theorem Th21: :: PARSP_2:21

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear holds
b₂,b₃ '||' b₄,b₅

proof end;

theorem Th22: :: PARSP_2:22

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅ being Element of b₁ st not b₂,b₃,b₄ is_collinear & b₂,b₃ '||' b₄,b₅ holds
not b₂,b₃,b₅ is_collinear

proof end;

theorem Th23: :: PARSP_2:23

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st not b₂,b₃,b₄ is_collinear & b₂,b₃ '||' b₄,b₅ & b₄ <> b₅ & b₂,b₃,b₆ is_collinear holds
not b₄,b₅,b₆ is_collinear

proof end;

theorem Th24: :: PARSP_2:24

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅ being Element of b₁ holds
( b₂,b₃,b₄ is_collinear or not b₂,b₃,b₅ is_collinear or not b₂,b₄,b₅ is_collinear or b₂ = b₅ )

proof end;

theorem Th25: :: PARSP_2:25

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st b₂ <> b₃ & b₂ <> b₄ & b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear & b₂,b₄,b₆ is_collinear holds
b₃,b₄ '||' b₅,b₆

proof end;

theorem Th26: :: PARSP_2:26

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st not b₂,b₃ '||' b₄,b₅ & b₂,b₃,b₆ is_collinear & b₂,b₃,b₇ is_collinear & b₄,b₅,b₆ is_collinear & b₄,b₅,b₇ is_collinear holds
b₆ = b₇

proof end;

theorem Th27: :: PARSP_2:27

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ <> b₃ & b₂,b₃,b₄ is_collinear & b₂,b₃ '||' b₄,b₅ holds
b₂,b₄ '||' b₃,b₅

proof end;

theorem Th28: :: PARSP_2:28

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ <> b₃ & b₂,b₃,b₄ is_collinear & b₂,b₃ '||' b₄,b₅ holds
b₄,b₃ '||' b₄,b₅

proof end;

theorem Th29: :: PARSP_2:29

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st not b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear & b₂,b₄,b₆ is_collinear & b₂,b₄,b₇ is_collinear & b₃,b₄ '||' b₅,b₆ & b₃,b₄ '||' b₅,b₇ holds
b₆ = b₇

proof end;

theorem Th30: :: PARSP_2:30

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ <> b₃ & b₂,b₃,b₄ is_collinear & b₂,b₃,b₅ is_collinear holds
b₂,b₄,b₅ is_collinear

proof end;

theorem Th31: :: PARSP_2:31

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃,b₄ is_collinear & b₂,b₄,b₅ is_collinear & b₂ <> b₄ holds
b₃,b₄,b₅ is_collinear

proof end;

definition

let c₁ be FanodesSp;
let c₂, c₃, c₄, c₅ be Element of c₁;
pred parallelogram c₂,c₃,c₄,c₅ means :Def3: :: PARSP_2:def 3
( not a₂,a₃,a₄ is_collinear & a₂,a₃ '||' a₄,a₅ & a₂,a₄ '||' a₃,a₅ );

end;

:: deftheorem Def3 defines parallelogram PARSP_2:def 3 :

theorem Th32: :: PARSP_2:32

canceled;

theorem Th33: :: PARSP_2:33

canceled;

theorem Th34: :: PARSP_2:34

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ holds
( b₂ <> b₃ & b₃ <> b₄ & b₄ <> b₂ & b₂ <> b₅ & b₃ <> b₅ & b₄ <> b₅ )

proof end;

theorem Th35: :: PARSP_2:35

proof end;

theorem Th36: :: PARSP_2:36

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ holds
( not b₂,b₃,b₄ is_collinear & not b₃,b₂,b₅ is_collinear & not b₄,b₅,b₂ is_collinear & not b₅,b₄,b₃ is_collinear & not b₂,b₄,b₃ is_collinear & not b₃,b₂,b₄ is_collinear & not b₃,b₄,b₂ is_collinear & not b₄,b₂,b₃ is_collinear & not b₄,b₃,b₂ is_collinear & not b₃,b₅,b₂ is_collinear & not b₂,b₃,b₅ is_collinear & not b₂,b₅,b₃ is_collinear & not b₅,b₂,b₃ is_collinear & not b₅,b₃,b₂ is_collinear & not b₄,b₂,b₅ is_collinear & not b₂,b₄,b₅ is_collinear & not b₂,b₅,b₄ is_collinear & not b₅,b₂,b₄ is_collinear & not b₅,b₄,b₂ is_collinear & not b₅,b₃,b₄ is_collinear & not b₃,b₄,b₅ is_collinear & not b₃,b₅,b₄ is_collinear & not b₄,b₃,b₅ is_collinear & not b₄,b₅,b₃ is_collinear )

proof end;

theorem Th37: :: PARSP_2:37

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ holds
( not parallelogram b₂,b₃,b₄,b₅ or not b₂,b₃,b₆ is_collinear or not b₄,b₅,b₆ is_collinear )

proof end;

theorem Th38: :: PARSP_2:38

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ holds
parallelogram b₂,b₄,b₃,b₅

proof end;

theorem Th39: :: PARSP_2:39

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ holds
parallelogram b₄,b₅,b₂,b₃

proof end;

theorem Th40: :: PARSP_2:40

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ holds
parallelogram b₃,b₂,b₅,b₄

proof end;

theorem Th41: :: PARSP_2:41

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ holds
( parallelogram b₂,b₄,b₃,b₅ & parallelogram b₄,b₅,b₂,b₃ & parallelogram b₃,b₂,b₅,b₄ & parallelogram b₄,b₂,b₅,b₃ & parallelogram b₅,b₃,b₄,b₂ & parallelogram b₃,b₅,b₂,b₄ & parallelogram b₅,b₄,b₃,b₂ )

proof end;

theorem Th42: :: PARSP_2:42

for b₁ being FanodesSp
for b₂, b₃, b₄ being Element of b₁ st not b₂,b₃,b₄ is_collinear holds
ex b₅ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅

proof end;

theorem Th43: :: PARSP_2:43

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ & parallelogram b₂,b₃,b₄,b₆ holds
b₅ = b₆

proof end;

theorem Th44: :: PARSP_2:44

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ holds
not b₂,b₅ '||' b₃,b₄

proof end;

theorem Th45: :: PARSP_2:45

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ holds
not parallelogram b₂,b₃,b₅,b₄

proof end;

theorem Th46: :: PARSP_2:46

for b₁ being FanodesSp
for b₂, b₃ being Element of b₁ st b₂ <> b₃ holds
ex b₄ being Element of b₁ st
( b₂,b₃,b₄ is_collinear & b₄ <> b₂ & b₄ <> b₃ )

proof end;

theorem Th47: :: PARSP_2:47

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ & parallelogram b₂,b₃,b₆,b₇ holds
b₄,b₆ '||' b₅,b₇

proof end;

theorem Th48: :: PARSP_2:48

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st not b₂,b₃,b₄ is_collinear & parallelogram b₅,b₆,b₂,b₃ & parallelogram b₅,b₆,b₄,b₇ holds
parallelogram b₂,b₃,b₄,b₇

proof end;

theorem Th49: :: PARSP_2:49

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st b₂,b₃,b₄ is_collinear & b₃ <> b₄ & parallelogram b₂,b₅,b₃,b₆ & parallelogram b₂,b₅,b₄,b₇ holds
parallelogram b₃,b₆,b₄,b₇

proof end;

theorem Th50: :: PARSP_2:50

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ & parallelogram b₂,b₃,b₆,b₇ & parallelogram b₄,b₅,b₈,b₉ holds
b₆,b₈ '||' b₇,b₉

proof end;

theorem Th51: :: PARSP_2:51

for b₁ being FanodesSp
for b₂, b₃ being Element of b₁ st b₂ <> b₃ holds
ex b₄, b₅ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅

proof end;

theorem Th52: :: PARSP_2:52

for b₁ being FanodesSp
for b₂, b₃ being Element of b₁ st b₂ <> b₃ holds
ex b₄, b₅ being Element of b₁ st parallelogram b₂,b₄,b₅,b₃

proof end;

definition

let c₁ be FanodesSp;
let c₂, c₃, c₄, c₅ be Element of c₁;
pred c₂,c₃ congr c₄,c₅ means :Def4: :: PARSP_2:def 4
( ( a₂ = a₃ & a₄ = a₅ ) or ex b₁, b₂ being Element of a₁ st
( parallelogram b₁,b₂,a₂,a₃ & parallelogram b₁,b₂,a₄,a₅ ) );

end;

:: deftheorem Def4 defines congr PARSP_2:def 4 :

theorem Th53: :: PARSP_2:53

canceled;

theorem Th54: :: PARSP_2:54

canceled;

theorem Th55: :: PARSP_2:55

for b₁ being FanodesSp
for b₂, b₃, b₄ being Element of b₁ st b₂,b₂ congr b₃,b₄ holds
b₃ = b₄

proof end;

theorem Th56: :: PARSP_2:56

for b₁ being FanodesSp
for b₂, b₃, b₄ being Element of b₁ st b₂,b₃ congr b₄,b₄ holds
b₂ = b₃

proof end;

theorem Th57: :: PARSP_2:57

for b₁ being FanodesSp
for b₂, b₃ being Element of b₁ st b₂,b₃ congr b₃,b₂ holds
b₂ = b₃

proof end;

theorem Th58: :: PARSP_2:58

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ congr b₄,b₅ holds
b₂,b₃ '||' b₄,b₅

proof end;

theorem Th59: :: PARSP_2:59

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ congr b₄,b₅ holds
b₂,b₄ '||' b₃,b₅

proof end;

theorem Th60: :: PARSP_2:60

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ congr b₄,b₅ & not b₂,b₃,b₄ is_collinear holds
parallelogram b₂,b₃,b₄,b₅

proof end;

theorem Th61: :: PARSP_2:61

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅ being Element of b₁ st parallelogram b₂,b₃,b₄,b₅ holds
b₂,b₃ congr b₄,b₅

proof end;

theorem Th62: :: PARSP_2:62

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st b₂,b₃ congr b₄,b₅ & b₂,b₃,b₄ is_collinear & parallelogram b₆,b₇,b₂,b₃ holds
parallelogram b₆,b₇,b₄,b₅

proof end;

theorem Th63: :: PARSP_2:63

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st b₂,b₃ congr b₄,b₅ & b₂,b₃ congr b₄,b₆ holds
b₅ = b₆

proof end;

theorem Th64: :: PARSP_2:64

for b₁ being FanodesSp
for b₂, b₃, b₄ being Element of b₁ ex b₅ being Element of b₁ st b₂,b₃ congr b₄,b₅

proof end;

theorem Th65: :: PARSP_2:65

canceled;

theorem Th66: :: PARSP_2:66

for b₁ being FanodesSp
for b₂, b₃ being Element of b₁ holds b₂,b₃ congr b₂,b₃

proof end;

theorem Th67: :: PARSP_2:67

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅, b₆, b₇ being Element of b₁ st b₂,b₃ congr b₄,b₅ & b₂,b₃ congr b₆,b₇ holds
b₄,b₅ congr b₆,b₇

proof end;

theorem Th68: :: PARSP_2:68

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ congr b₄,b₅ holds
b₄,b₅ congr b₂,b₃

proof end;

theorem Th69: :: PARSP_2:69

for b₁ being FanodesSp
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂,b₃ congr b₄,b₅ holds
b₃,b₂ congr b₅,b₄

proof end;