:: 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

definition

let F be Field;

ex b_{1} 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_{1} . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))]

for b_{1}, b_{2} 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_{1} . (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_{2} . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] ) holds

b_{1} = b_{2}

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

ex b

for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines c3add PARSP_1:def 1 :

for F being Field

for b_{2} being BinOp of [: the carrier of F, the carrier of F, the carrier of F:] holds

( b_{2} = c3add F iff for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b_{2} . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] );

for F being Field

for b

( b

definition

let F be Field;

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

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

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

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

:: 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);

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

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)]

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;

ex b_{1} 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_{1} . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))]

for b_{1}, b_{2} 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_{1} . 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_{2} . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))] ) holds

b_{1} = b_{2}

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

ex b

for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines c3compl PARSP_1:def 3 :

for F being Field

for b_{2} being UnOp of [: the carrier of F, the carrier of F, the carrier of F:] holds

( b_{2} = c3compl F iff for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b_{2} . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))] );

for F being Field

for b

( b

definition

let F be Field;

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

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

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

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

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

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

definition

attr c_{1} is strict ;

struct ParStr -> 1-sorted ;

aggr ParStr(# carrier, CONGR #) -> ParStr ;

sel CONGR c_{1} -> Relation of [: the carrier of c_{1}, the carrier of c_{1}:];

end;
struct ParStr -> 1-sorted ;

aggr ParStr(# carrier, CONGR #) -> ParStr ;

sel CONGR c

registration
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 );

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
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:];

for F being Field holds C_3 F = [: the carrier of F, the carrier of F, the carrier of F:];

:: 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):]:];

for F being Field holds 4C_3 F = [:[:(C_3 F),(C_3 F):],[:(C_3 F),(C_3 F):]:];

definition

let F be Field;

ex b_{1} being set st

for x being object holds

( x in b_{1} 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 b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} 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_{2} 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_{1} = b_{2}

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

ex b

for x being object holds

( x in b

( 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

( x in b

( 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

( 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

proof end;

:: deftheorem Def8 defines PRs PARSP_1:def 9 :

for F being Field

for b_{2} being set holds

( b_{2} = PRs F iff for x being object holds

( x in b_{2} 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 F being Field

for b

( b

( x in b

( 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 ) ) ) );

:: deftheorem defines MPS PARSP_1:def 11 :

for F being Field holds MPS F = ParStr(# (C_3 F),(PR F) #);

for F being Field holds MPS F = ParStr(# (C_3 F),(PR F) #);

theorem :: PARSP_1:7

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;

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;

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

theorem :: PARSP_1:11

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 ) )

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

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 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 )

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

::

:: 3. DEFINITION OF PARALLELITY SPACE

::

definition

let IT be non empty ParStr ;

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

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

:: 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 ) ) );

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
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 )

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 )

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

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

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

theorem :: PARSP_1:28

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 )

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

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

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

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

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

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

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

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

( 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

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;

:: 2. PARALLELITY STRUCTURE

::