:: Parallelity Spaces
:: by Eugeniusz Kusak, Wojciech Leo\'nczuk and Micha{\l} Muzalewski
::
:: Received November 23, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users

Lm1: for F being non empty right_complementable add-associative right_zeroed addLoopStr
for a, b being Element of F holds - (a - b) = b - a

proof end;

Lm2: for F being Field
for a, b, c, d being Element of F holds ((a - b) * (c - d)) - ((b - a) * (d - c)) = 0. F

proof end;

Lm3: for F being Field
for a, b, c, d being Element of F holds (a * (b - b)) - ((c - c) * d) = 0. F

proof end;

Lm4: for F being Field
for a, b, c, d, e, h being Element of F st a <> 0. F & (a * e) - (d * b) = 0. F & (a * c) - (h * b) = 0. F holds
(d * c) - (h * e) = 0. F

proof end;

Lm5: for F being Field
for a, b, c, d being Element of F st (a * b) - (c * d) = 0. F holds
(d * c) - (b * a) = 0. F

proof end;

Lm6: for F being Field
for a, b, c, d, e, h being Element of F st b <> 0. F & (a * e) - (d * b) = 0. F & (a * c) - (h * b) = 0. F holds
(d * c) - (h * e) = 0. F

proof end;

Lm7: for F being Field
for a, b, c, d being Element of F holds (c * d) * (a * b) = ((a * c) * d) * b

proof end;

Lm8: for F being Field
for a, b, c, d, f, g being Element of F st (a * b) - (c * d) = 0. F holds
(((a * f) * g) * b) - (((c * f) * g) * d) = 0. F

proof end;

Lm9: for F being Field
for a, b, c, d being Element of F holds (a - b) * (c - d) = (a * c) + ((- (a * d)) + (- (b * (c - d))))

proof end;

Lm10: for F being Field
for a, b, c, d being Element of F holds (a + b) + (c + d) = (a + (b + c)) + d

proof end;

Lm11: for F being non empty right_complementable add-associative right_zeroed addLoopStr
for a, b, c being Element of F holds (b + a) - (c + a) = b - c

proof end;

Lm12: for F being non empty right_complementable add-associative right_zeroed addLoopStr
for a, b being Element of F holds a + b = - ((- b) + (- a))

proof end;

Lm13: for F being Field
for a, b, c, d, e, f being Element of F st ((a - b) * (c - d)) - ((a - e) * (c - f)) = 0. F holds
((b - a) * (f - d)) - ((b - e) * (f - c)) = 0. F

proof end;

Lm14: for F being Field
for a, b, c being Element of F holds a - ((a + b) + (- c)) = c - b

proof end;

Lm15: for F being Field
for a, b, c, e, g, h being Element of F holds ((a - b) * (c - ((c + h) + (- g)))) - ((e - ((e + b) + (- a))) * (g - h)) = 0. F

proof end;

deffunc H₁( Field) -> set = [: the carrier of $1, the carrier of $1, the carrier of $1:];

definition

let F be Field;

func c3add F -> BinOp of [: the carrier of F, the carrier of F, the carrier of F:] means :Def1: :: PARSP_1:def 1
for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds it . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))];

existence
ex b₁ being BinOp of [: the carrier of F, the carrier of F, the carrier of F:] st
for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b₁ . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))]

proof end;

uniqueness
for b₁, b₂ being BinOp of [: the carrier of F, the carrier of F, the carrier of F:] st ( for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b₁ . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] ) & ( for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b₂ . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines c3add PARSP_1:def 1 :
for F being Field
for b₂ being BinOp of [: the carrier of F, the carrier of F, the carrier of F:] holds
( b₂ = c3add F iff for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b₂ . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] );

definition

let F be Field;
let x, y be Element of [: the carrier of F, the carrier of F, the carrier of F:];

func x + y -> Element of [: the carrier of F, the carrier of F, the carrier of F:] equals :: PARSP_1:def 2
(c3add F) . (x,y);

coherence
(c3add F) . (x,y) is Element of [: the carrier of F, the carrier of F, the carrier of F:] ;

end;

:: deftheorem defines + PARSP_1:def 2 :
for F being Field
for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds x + y = (c3add F) . (x,y);

theorem :: PARSP_1:1

for F being Field
for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds x + y = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] by Def1;

theorem Th2: :: PARSP_1:2

for F being Field
for a, b, c, f, g, h being Element of F holds [a,b,c] + [f,g,h] = [(a + f),(b + g),(c + h)]

proof end;

definition

let F be Field;

func c3compl F -> UnOp of [: the carrier of F, the carrier of F, the carrier of F:] means :Def3: :: PARSP_1:def 3
for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds it . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))];

existence
ex b₁ being UnOp of [: the carrier of F, the carrier of F, the carrier of F:] st
for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b₁ . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))]

proof end;

uniqueness
for b₁, b₂ being UnOp of [: the carrier of F, the carrier of F, the carrier of F:] st ( for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b₁ . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))] ) & ( for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b<sub>2</sub> . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines c3compl PARSP_1:def 3 :
for F being Field
for b₂ being UnOp of [: the carrier of F, the carrier of F, the carrier of F:] holds
( b₂ = c3compl F iff for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b₂ . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))] );

definition

let F be Field;
let x be Element of [: the carrier of F, the carrier of F, the carrier of F:];

func - x -> Element of [: the carrier of F, the carrier of F, the carrier of F:] equals :: PARSP_1:def 4
(c3compl F) . x;

coherence
(c3compl F) . x is Element of [: the carrier of F, the carrier of F, the carrier of F:] ;

end;

:: deftheorem defines - PARSP_1:def 4 :
for F being Field
for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds - x = (c3compl F) . x;

theorem :: PARSP_1:3

for F being Field
for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds - x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))] by Def3;

::
:: 2. PARALLELITY STRUCTURE
::

definition

attr c₁ is strict ;
struct ParStr -> 1-sorted ;
aggr ParStr(# carrier, CONGR #) -> ParStr ;
sel CONGR c₁ -> Relation of [: the carrier of c₁, the carrier of c₁:];

end;

:: deftheorem PARSP_1:def 5 :
canceled;

registration

cluster non empty for ParStr ;

existence
not for b₁ being ParStr holds b₁ is empty

proof end;

end;

definition

let PS be non empty ParStr ;
let a, b, c, d be Element of PS;

pred a,b '||' c,d means :: PARSP_1:def 6
[[a,b],[c,d]] in the CONGR of PS;

end;

:: deftheorem defines '||' PARSP_1:def 6 :
for PS being non empty ParStr
for a, b, c, d being Element of PS holds
( a,b '||' c,d iff [[a,b],[c,d]] in the CONGR of PS );

definition

let F be Field;

func C_3 F -> set equals :: PARSP_1:def 7
[: the carrier of F, the carrier of F, the carrier of F:];

coherence
[: the carrier of F, the carrier of F, the carrier of F:] is set ;

end;

:: deftheorem defines C_3 PARSP_1:def 7 :
for F being Field holds C_3 F = [: the carrier of F, the carrier of F, the carrier of F:];

registration

let F be Field;

cluster C_3 F -> non empty ;

coherence
not C_3 F is empty ;

end;

definition

let F be Field;

func 4C_3 F -> set equals :: PARSP_1:def 8
[:[:(C_3 F),(C_3 F):],[:(C_3 F),(C_3 F):]:];

coherence
[:[:(C_3 F),(C_3 F):],[:(C_3 F),(C_3 F):]:] is set ;

end;

:: deftheorem defines 4C_3 PARSP_1:def 8 :
for F being Field holds 4C_3 F = [:[:(C_3 F),(C_3 F):],[:(C_3 F),(C_3 F):]:];

registration

let F be Field;

cluster 4C_3 F -> non empty ;

coherence
not 4C_3 F is empty ;

end;

definition

let F be Field;

func PRs F -> set means :Def8: :: PARSP_1:def 9
for x being object holds
( x in it iff ( x in 4C_3 F & ex a, b, c, d being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( x = [[a,b],[c,d]] & (((a `1_3) - (b `1_3)) * ((c `2_3) - (d `2_3))) - (((c `1_3) - (d `1_3)) * ((a `2_3) - (b `2_3))) = 0. F & (((a `1_3) - (b `1_3)) * ((c `3_3) - (d `3_3))) - (((c `1_3) - (d `1_3)) * ((a `3_3) - (b `3_3))) = 0. F & (((a `2_3) - (b `2_3)) * ((c `3_3) - (d `3_3))) - (((c `2_3) - (d `2_3)) * ((a `3_3) - (b `3_3))) = 0. F ) ) );

existence
ex b₁ being set st
for x being object holds
( x in b₁ iff ( x in 4C_3 F & ex a, b, c, d being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( x = [[a,b],[c,d]] & (((a `1_3) - (b `1_3)) * ((c `2_3) - (d `2_3))) - (((c `1_3) - (d `1_3)) * ((a `2_3) - (b `2_3))) = 0. F & (((a `1_3) - (b `1_3)) * ((c `3_3) - (d `3_3))) - (((c `1_3) - (d `1_3)) * ((a `3_3) - (b `3_3))) = 0. F & (((a `2_3) - (b `2_3)) * ((c `3_3) - (d `3_3))) - (((c `2_3) - (d `2_3)) * ((a `3_3) - (b `3_3))) = 0. F ) ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff ( x in 4C_3 F & ex a, b, c, d being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( x = [[a,b],[c,d]] & (((a `1_3) - (b `1_3)) * ((c `2_3) - (d `2_3))) - (((c `1_3) - (d `1_3)) * ((a `2_3) - (b `2_3))) = 0. F & (((a `1_3) - (b `1_3)) * ((c `3_3) - (d `3_3))) - (((c `1_3) - (d `1_3)) * ((a `3_3) - (b `3_3))) = 0. F & (((a `2_3) - (b `2_3)) * ((c `3_3) - (d `3_3))) - (((c `2_3) - (d `2_3)) * ((a `3_3) - (b `3_3))) = 0. F ) ) ) ) & ( for x being object holds
( x in b₂ iff ( x in 4C_3 F & ex a, b, c, d being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( x = [[a,b],[c,d]] & (((a `1_3) - (b `1_3)) * ((c `2_3) - (d `2_3))) - (((c `1_3) - (d `1_3)) * ((a `2_3) - (b `2_3))) = 0. F & (((a `1_3) - (b `1_3)) * ((c `3_3) - (d `3_3))) - (((c `1_3) - (d `1_3)) * ((a `3_3) - (b `3_3))) = 0. F & (((a `2_3) - (b `2_3)) * ((c `3_3) - (d `3_3))) - (((c `2_3) - (d `2_3)) * ((a `3_3) - (b `3_3))) = 0. F ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines PRs PARSP_1:def 9 :
for F being Field
for b₂ being set holds
( b₂ = PRs F iff for x being object holds
( x in b₂ iff ( x in 4C_3 F & ex a, b, c, d being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( x = [[a,b],[c,d]] & (((a `1_3) - (b `1_3)) * ((c `2_3) - (d `2_3))) - (((c `1_3) - (d `1_3)) * ((a `2_3) - (b `2_3))) = 0. F & (((a `1_3) - (b `1_3)) * ((c `3_3) - (d `3_3))) - (((c `1_3) - (d `1_3)) * ((a `3_3) - (b `3_3))) = 0. F & (((a `2_3) - (b `2_3)) * ((c `3_3) - (d `3_3))) - (((c `2_3) - (d `2_3)) * ((a `3_3) - (b `3_3))) = 0. F ) ) ) );

theorem Th4: :: PARSP_1:4

for F being Field holds PRs F c= [:[:(C_3 F),(C_3 F):],[:(C_3 F),(C_3 F):]:]

proof end;

definition

let F be Field;

func PR F -> Relation of [:(C_3 F),(C_3 F):] equals :: PARSP_1:def 10
PRs F;

coherence
PRs F is Relation of [:(C_3 F),(C_3 F):] by Th4;

end;

:: deftheorem defines PR PARSP_1:def 10 :
for F being Field holds PR F = PRs F;

definition

let F be Field;

func MPS F -> ParStr equals :: PARSP_1:def 11
ParStr(# (C_3 F),(PR F) #);

correctness
coherence
ParStr(# (C_3 F),(PR F) #) is ParStr ;
;

end;

:: deftheorem defines MPS PARSP_1:def 11 :
for F being Field holds MPS F = ParStr(# (C_3 F),(PR F) #);

registration

let F be Field;

cluster MPS F -> non empty strict ;

coherence
( MPS F is strict & not MPS F is empty ) ;

end;

theorem :: PARSP_1:5

for F being Field holds the carrier of (MPS F) = C_3 F ;

theorem :: PARSP_1:6

for F being Field holds the CONGR of (MPS F) = PR F ;

theorem :: PARSP_1:7

for F being Field
for a, b, c, d being Element of (MPS F) holds
( a,b '||' c,d iff [[a,b],[c,d]] in PR F ) ;

theorem :: PARSP_1:8

for F being Field
for a, b, c, d being Element of (MPS F) holds
( [[a,b],[c,d]] in PR F iff ( [[a,b],[c,d]] in 4C_3 F & ex e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( [[a,b],[c,d]] = [[e,f],[g,h]] & (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F & (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F ) ) ) by Def8;

theorem Th9: :: PARSP_1:9

for F being Field
for a, b, c, d being Element of (MPS F) holds
( a,b '||' c,d iff ( [[a,b],[c,d]] in 4C_3 F & ex e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( [[a,b],[c,d]] = [[e,f],[g,h]] & (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F & (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F ) ) ) by Def8;

theorem :: PARSP_1:10

for F being Field holds the carrier of (MPS F) = [: the carrier of F, the carrier of F, the carrier of F:] ;

theorem :: PARSP_1:11

for F being Field
for a, b, c, d being Element of (MPS F) holds [[a,b],[c,d]] in 4C_3 F ;

theorem Th12: :: PARSP_1:12

for F being Field
for a, b, c, d being Element of (MPS F) holds
( a,b '||' c,d iff ex e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( [[a,b],[c,d]] = [[e,f],[g,h]] & (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F & (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F ) )

proof end;

theorem Th13: :: PARSP_1:13

for F being Field
for a, b being Element of (MPS F) holds a,b '||' b,a

proof end;

theorem Th14: :: PARSP_1:14

for F being Field
for a, b, c being Element of (MPS F) holds a,b '||' c,c

proof end;

theorem Th15: :: PARSP_1:15

for F being Field
for a, b, p, q, r, s being Element of (MPS F) st a,b '||' p,q & a,b '||' r,s & not p,q '||' r,s holds
a = b

proof end;

theorem Th16: :: PARSP_1:16

for F being Field
for a, b, c being Element of (MPS F) st a,b '||' a,c holds
b,a '||' b,c

proof end;

theorem Th17: :: PARSP_1:17

for F being Field
for a, b, c being Element of (MPS F) ex d being Element of (MPS F) st
( a,b '||' c,d & a,c '||' b,d )

proof end;

::
:: 3. DEFINITION OF PARALLELITY SPACE
::

definition

let IT be non empty ParStr ;

attr IT is ParSp-like means :Def11: :: PARSP_1:def 12
for a, b, c, d, p, q, r, s being Element of IT holds
( a,b '||' b,a & a,b '||' c,c & ( a,b '||' p,q & a,b '||' r,s & not p,q '||' r,s implies a = b ) & ( a,b '||' a,c implies b,a '||' b,c ) & ex x being Element of IT st
( a,b '||' c,x & a,c '||' b,x ) );

end;

:: deftheorem Def11 defines ParSp-like PARSP_1:def 12 :
for IT being non empty ParStr holds
( IT is ParSp-like iff for a, b, c, d, p, q, r, s being Element of IT holds
( a,b '||' b,a & a,b '||' c,c & ( a,b '||' p,q & a,b '||' r,s & not p,q '||' r,s implies a = b ) & ( a,b '||' a,c implies b,a '||' b,c ) & ex x being Element of IT st
( a,b '||' c,x & a,c '||' b,x ) ) );

registration

cluster non empty strict ParSp-like for ParStr ;

existence
ex b₁ being non empty ParStr st
( b₁ is strict & b₁ is ParSp-like )

proof end;

end;

definition

mode ParSp is non empty ParSp-like ParStr ;

end;

theorem Th18: :: PARSP_1:18

for PS being ParSp
for a, b being Element of PS holds a,b '||' a,b

proof end;

theorem Th19: :: PARSP_1:19

for PS being ParSp
for a, b, c, d being Element of PS st a,b '||' c,d holds
c,d '||' a,b

proof end;

theorem Th20: :: PARSP_1:20

for PS being ParSp
for a, b, c being Element of PS holds a,a '||' b,c

proof end;

theorem Th21: :: PARSP_1:21

for PS being ParSp
for a, b, c, d being Element of PS st a,b '||' c,d holds
b,a '||' c,d

proof end;

theorem Th22: :: PARSP_1:22

for PS being ParSp
for a, b, c, d being Element of PS st a,b '||' c,d holds
a,b '||' d,c

proof end;

theorem Th23: :: PARSP_1:23

for PS being ParSp
for a, b, c, d being Element of PS st a,b '||' c,d holds
( b,a '||' c,d & a,b '||' d,c & b,a '||' d,c & c,d '||' a,b & d,c '||' a,b & c,d '||' b,a & d,c '||' b,a )

proof end;

theorem Th24: :: PARSP_1:24

for PS being ParSp
for a, b, c being Element of PS st a,b '||' a,c holds
( a,c '||' a,b & b,a '||' a,c & a,b '||' c,a & a,c '||' b,a & b,a '||' c,a & c,a '||' a,b & c,a '||' b,a & b,a '||' b,c & a,b '||' b,c & b,a '||' c,b & b,c '||' b,a & a,b '||' c,b & c,b '||' b,a & b,c '||' a,b & c,b '||' a,b & c,a '||' c,b & a,c '||' c,b & c,a '||' b,c & a,c '||' b,c & c,b '||' c,a & b,c '||' c,a & c,b '||' a,c & b,c '||' a,c )

proof end;

theorem :: PARSP_1:25

for PS being ParSp
for a, b, c, d being Element of PS st ( a = b or c = d or ( a = c & b = d ) or ( a = d & b = c ) ) holds
a,b '||' c,d by Def11, Th18, Th20;

theorem Th26: :: PARSP_1:26

for PS being ParSp
for a, b, p, q, r, s being Element of PS st a <> b & p,q '||' a,b & a,b '||' r,s holds
p,q '||' r,s

proof end;

theorem :: PARSP_1:27

for PS being ParSp
for a, b, c being Element of PS st not a,b '||' a,c holds
( a <> b & b <> c & c <> a ) by Def11, Th18, Th20;

theorem :: PARSP_1:28

for PS being ParSp
for a, b, c, d being Element of PS st not a,b '||' c,d holds
( a <> b & c <> d ) by Def11, Th20;

theorem Th29: :: PARSP_1:29

for PS being ParSp
for a, b, c being Element of PS st not a,b '||' a,c holds
( not a,c '||' a,b & not b,a '||' a,c & not a,b '||' c,a & not a,c '||' b,a & not b,a '||' c,a & not c,a '||' a,b & not c,a '||' b,a & not b,a '||' b,c & not a,b '||' b,c & not b,a '||' c,b & not b,c '||' b,a & not b,a '||' c,b & not c,b '||' b,a & not b,c '||' a,b & not c,b '||' a,b & not c,a '||' c,b & not a,c '||' c,b & not c,a '||' b,c & not a,c '||' b,c & not c,b '||' c,a & not b,c '||' c,a & not c,b '||' a,c & not b,c '||' a,c )

proof end;

theorem Th30: :: PARSP_1:30

for PS being ParSp
for a, b, c, d, p, q, r, s being Element of PS st not a,b '||' c,d & a,b '||' p,q & c,d '||' r,s & p <> q & r <> s holds
not p,q '||' r,s

proof end;

theorem Th31: :: PARSP_1:31

for PS being ParSp
for a, b, c, p, q, r being Element of PS st not a,b '||' a,c & a,b '||' p,q & a,c '||' p,r & b,c '||' q,r & p <> q holds
not p,q '||' p,r

proof end;

theorem Th32: :: PARSP_1:32

for PS being ParSp
for a, b, c, p, r being Element of PS st not a,b '||' a,c & a,c '||' p,r & b,c '||' p,r holds
p = r

proof end;

theorem Th33: :: PARSP_1:33

for PS being ParSp
for p, q, r, s being Element of PS st not p,q '||' p,r & p,r '||' p,s & q,r '||' q,s holds
r = s

proof end;

theorem :: PARSP_1:34

for PS being ParSp
for a, b, c, p, q, r, s being Element of PS st not a,b '||' a,c & a,b '||' p,q & a,c '||' p,r & a,c '||' p,s & b,c '||' q,r & b,c '||' q,s holds
r = s

proof end;

theorem Th35: :: PARSP_1:35

for PS being ParSp
for a, b, c, d being Element of PS st a,b '||' a,c & a,b '||' a,d holds
a,b '||' c,d

proof end;

theorem :: PARSP_1:36

for PS being ParSp st ( for a, b being Element of PS holds a = b ) holds
for p, q, r, s being Element of PS holds p,q '||' r,s

proof end;

theorem :: PARSP_1:37

for PS being ParSp st ex a, b being Element of PS st
( a <> b & ( for c being Element of PS holds a,b '||' a,c ) ) holds
for p, q, r, s being Element of PS holds p,q '||' r,s

proof end;

theorem :: PARSP_1:38

for PS being ParSp
for a, b, c, p, q being Element of PS st not a,b '||' a,c & p <> q & p,q '||' p,a & p,q '||' p,b holds
not p,q '||' p,c

proof end;