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


begin

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, e, d, b, c, 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 b, a, e, d, c, 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 c, d, a, b 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, h, g, e being Element of F holds ((a - b) * (c - ((c + h) + (- g)))) - ((e - ((e + b) + (- a))) * (g - h)) = 0. F

proof end;

deffunc H1( 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 b1 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 b1 . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))]
proof end;
uniqueness
for b1, b2 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 b1 . (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 b2 . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines c3add PARSP_1:def 1 :
for F being Field
for b2 being BinOp of [: the carrier of F, the carrier of F, the carrier of F:] holds
( b2 = c3add F iff for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b2 . (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 b1 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 b1 . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))]
proof end;
uniqueness
for b1, b2 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 b1 . 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 b2 . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines c3compl PARSP_1:def 3 :
for F being Field
for b2 being UnOp of [: the carrier of F, the carrier of F, the carrier of F:] holds
( b2 = c3compl F iff for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b2 . 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;

definition
let S be set ;
mode Relation4 of S -> set means :Def5: :: PARSP_1:def 5
it c= [:S,S,S,S:];
existence
ex b1 being set st b1 c= [:S,S,S,S:]
;
end;

:: deftheorem Def5 defines Relation4 PARSP_1:def 5 :
for S, b2 being set holds
( b2 is Relation4 of S iff b2 c= [:S,S,S,S:] );

definition
attr c1 is strict ;
struct ParStr -> 1-sorted ;
aggr ParStr(# carrier, 4_arg_relation #) -> ParStr ;
sel 4_arg_relation c1 -> Relation4 of the carrier of c1;
end;

registration
cluster non empty for ParStr ;
existence
not for b1 being ParStr holds b1 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 :Def6: :: PARSP_1:def 6
[a,b,c,d] in the 4_arg_relation of PS;
end;

:: deftheorem Def6 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 4_arg_relation 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 :Def9: :: PARSP_1:def 9
for x being set 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 b1 being set st
for x being set holds
( x in b1 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 b1, b2 being set st ( for x being set holds
( x in b1 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 set holds
( x in b2 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
b1 = b2
proof end;
end;

:: deftheorem Def9 defines PRs PARSP_1:def 9 :
for F being Field
for b2 being set holds
( b2 = PRs F iff for x being set holds
( x in b2 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 -> Relation4 of C_3 F equals :: PARSP_1:def 10
PRs F;
coherence
PRs F is Relation4 of C_3 F
proof end;
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 4_arg_relation 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 ) by Def6;

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 Def9;

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 ) ) )
proof end;

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 :Def12: :: 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 Def12 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 b1 being non empty ParStr st
( b1 is strict & b1 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 Def12, 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 Def12, 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 Def12, 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;