:: PARSP_1 semantic presentation

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
let F be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for a, b being Element of F holds - (a - b) = b - a
let a, b be Element of F; ::_thesis: - (a - b) = b - a
thus  - (a - b) = b + (- a) by RLVECT_1:33
.= b - a by RLVECT_1:def_11 ; ::_thesis: verum
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
let F be Field; ::_thesis: for a, b, c, d being Element of F holds ((a - b) * (c - d)) - ((b - a) * (d - c)) = 0. F
let a, b, c, d be Element of F; ::_thesis: ((a - b) * (c - d)) - ((b - a) * (d - c)) = 0. F
 ( - (a - b) = b - a & - (c - d) = d - c ) by Lm1;
then  ((a - b) * (c - d)) - ((b - a) * (d - c)) = ((a - b) * (c - d)) - ((a - b) * (c - d)) by VECTSP_1:10;
hence  ((a - b) * (c - d)) - ((b - a) * (d - c)) = 0. F by RLVECT_1:15; ::_thesis: verum
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
let F be Field; ::_thesis: for a, b, c, d being Element of F holds (a * (b - b)) - ((c - c) * d) = 0. F
let a, b, c, d be Element of F; ::_thesis: (a * (b - b)) - ((c - c) * d) = 0. F
 c - c = 0. F by RLVECT_1:15;
then A1: (c - c) * d = 0. F by VECTSP_1:7;
 b - b = 0. F by RLVECT_1:15;
then  a * (b - b) = 0. F by VECTSP_1:7;
hence  (a * (b - b)) - ((c - c) * d) = 0. F by A1, RLVECT_1:15; ::_thesis: verum
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
let F be Field; ::_thesis: 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
let a, e, d, b, c, h be Element of F; ::_thesis: ( a <> 0. F & (a * e) - (d * b) = 0. F & (a * c) - (h * b) = 0. F implies (d * c) - (h * e) = 0. F )
assume that
A1: a <> 0. F and
A2: (a * e) - (d * b) = 0. F and
A3: (a * c) - (h * b) = 0. F ; ::_thesis: (d * c) - (h * e) = 0. F
 c = (h * b) * (a ") by A1, A3, VECTSP_1:30;
then  c = h * (b * (a ")) by GROUP_1:def_3;
then A4: d * c = (d * h) * (b * (a ")) by GROUP_1:def_3;
 e = (d * b) * (a ") by A1, A2, VECTSP_1:30;
then  e = d * (b * (a ")) by GROUP_1:def_3;
then  h * e = (h * d) * (b * (a ")) by GROUP_1:def_3;
hence  (d * c) - (h * e) = 0. F by A4, RLVECT_1:15; ::_thesis: verum
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
let F be Field; ::_thesis: for a, b, c, d being Element of F st (a * b) - (c * d) = 0. F holds
(d * c) - (b * a) = 0. F
let a, b, c, d be Element of F; ::_thesis: ( (a * b) - (c * d) = 0. F implies (d * c) - (b * a) = 0. F )
assume  (a * b) - (c * d) = 0. F ; ::_thesis: (d * c) - (b * a) = 0. F
then A1: - ((a * b) - (c * d)) = 0. F by RLVECT_1:12;
thus (d * c) - (b * a) = (d * c) + (- (b * a)) by RLVECT_1:def_11
.= 0. F by A1, RLVECT_1:33 ; ::_thesis: verum
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
let F be Field; ::_thesis: 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
let b, a, e, d, c, h be Element of F; ::_thesis: ( b <> 0. F & (a * e) - (d * b) = 0. F & (a * c) - (h * b) = 0. F implies (d * c) - (h * e) = 0. F )
assume  b <> 0. F ; ::_thesis: ( not (a * e) - (d * b) = 0. F or not (a * c) - (h * b) = 0. F or (d * c) - (h * e) = 0. F )
then  ( (b * d) - (e * a) = 0. F & (b * h) - (c * a) = 0. F implies (e * h) - (c * d) = 0. F ) by Lm4;
hence  ( not (a * e) - (d * b) = 0. F or not (a * c) - (h * b) = 0. F or (d * c) - (h * e) = 0. F ) by Lm5; ::_thesis: verum
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
let F be Field; ::_thesis: for c, d, a, b being Element of F holds (c * d) * (a * b) = ((a * c) * d) * b
let c, d, a, b be Element of F; ::_thesis: (c * d) * (a * b) = ((a * c) * d) * b
thus (c * d) * (a * b) = (a * (c * d)) * b by GROUP_1:def_3
.= ((a * c) * d) * b by GROUP_1:def_3 ; ::_thesis: verum
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
let F be Field; ::_thesis: 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
let a, b, c, d, f, g be Element of F; ::_thesis: ( (a * b) - (c * d) = 0. F implies (((a * f) * g) * b) - (((c * f) * g) * d) = 0. F )
assume A1: (a * b) - (c * d) = 0. F ; ::_thesis: (((a * f) * g) * b) - (((c * f) * g) * d) = 0. F
 ( ((a * f) * g) * b = (f * g) * (a * b) & ((c * f) * g) * d = (f * g) * (c * d) ) by Lm7;
hence (((a * f) * g) * b) - (((c * f) * g) * d) = (f * g) * ((a * b) - (c * d)) by VECTSP_1:11
.= 0. F by A1, VECTSP_1:7 ;
::_thesis: verum
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
let F be Field; ::_thesis: for a, b, c, d being Element of F holds (a - b) * (c - d) = (a * c) + ((- (a * d)) + (- (b * (c - d))))
let a, b, c, d be Element of F; ::_thesis: (a - b) * (c - d) = (a * c) + ((- (a * d)) + (- (b * (c - d))))
thus (a - b) * (c - d) = (a + (- b)) * (c - d) by RLVECT_1:def_11
.= (a * (c - d)) + ((- b) * (c - d)) by VECTSP_1:def_7
.= (a * (c - d)) + (- (b * (c - d))) by VECTSP_1:9
.= ((a * c) - (a * d)) + (- (b * (c - d))) by VECTSP_1:11
.= ((a * c) + (- (a * d))) + (- (b * (c - d))) by RLVECT_1:def_11
.= (a * c) + ((- (a * d)) + (- (b * (c - d)))) by RLVECT_1:def_3 ; ::_thesis: verum
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
let F be Field; ::_thesis: for a, b, c, d being Element of F holds (a + b) + (c + d) = (a + (b + c)) + d
let a, b, c, d be Element of F; ::_thesis: (a + b) + (c + d) = (a + (b + c)) + d
thus (a + b) + (c + d) = ((a + b) + c) + d by RLVECT_1:def_3
.= (a + (b + c)) + d by RLVECT_1:def_3 ; ::_thesis: verum
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
let F be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for a, b, c being Element of F holds (b + a) - (c + a) = b - c
let a, b, c be Element of F; ::_thesis: (b + a) - (c + a) = b - c
thus (b + a) - (c + a) = (b + a) + (- (c + a)) by RLVECT_1:def_11
.= (b + a) + ((- a) + (- c)) by RLVECT_1:31
.= ((b + a) + (- a)) + (- c) by RLVECT_1:def_3
.= (b + (a + (- a))) + (- c) by RLVECT_1:def_3
.= (b + (0. F)) + (- c) by RLVECT_1:def_10
.= b + (- c) by RLVECT_1:4
.= b - c by RLVECT_1:def_11 ; ::_thesis: verum
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
let F be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for a, b being Element of F holds a + b = - ((- b) + (- a))
let a, b be Element of F; ::_thesis: a + b = - ((- b) + (- a))
thus a + b = - (- (a + b)) by RLVECT_1:17
.= - ((- b) + (- a)) by RLVECT_1:31 ; ::_thesis: verum
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
let F be Field; ::_thesis: 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
let a, b, c, d, e, f be Element of F; ::_thesis: ( ((a - b) * (c - d)) - ((a - e) * (c - f)) = 0. F implies ((b - a) * (f - d)) - ((b - e) * (f - c)) = 0. F )
assume A1: ((a - b) * (c - d)) - ((a - e) * (c - f)) = 0. F ; ::_thesis: ((b - a) * (f - d)) - ((b - e) * (f - c)) = 0. F
A2: ( (a - b) * (c - d) = (a * c) + ((- (a * d)) + (- (b * (c - d)))) & (a - e) * (c - f) = (a * c) + ((- (a * f)) + (- (e * (c - f)))) ) by Lm9;
 ( (b - a) * (f - d) = (b * f) + ((- (b * d)) + (- (a * (f - d)))) & (b - e) * (f - c) = (b * f) + ((- (b * c)) + (- (e * (f - c)))) ) by Lm9;
hence ((b - a) * (f - d)) - ((b - e) * (f - c)) = ((- (b * d)) + (- (a * (f - d)))) - ((- (b * c)) + (- (e * (f - c)))) by Lm11
.= ((- (b * d)) + (- ((a * f) - (a * d)))) - ((- (b * c)) + (- (e * (f - c)))) by VECTSP_1:11
.= ((- (b * d)) + ((- (a * f)) + (a * d))) - ((- (b * c)) + (- (e * (f - c)))) by RLVECT_1:33
.= (((- (b * d)) + (a * d)) + (- (a * f))) - ((- (b * c)) + (- (e * (f - c)))) by RLVECT_1:def_3
.= (((a * d) + (- (b * d))) + (- (a * f))) + (- ((- (b * c)) + (- (e * (f - c))))) by RLVECT_1:def_11
.= (((a * d) + (- (b * d))) + (- (a * f))) + ((- (- (b * c))) + (- (- (e * (f - c))))) by RLVECT_1:31
.= (((a * d) + (- (b * d))) + (- (a * f))) + ((b * c) + (- (- (e * (f - c))))) by RLVECT_1:17
.= (((a * d) + (- (b * d))) + (- (a * f))) + ((b * c) + (e * (f - c))) by RLVECT_1:17
.= (((a * d) + (- (b * d))) + ((- (a * f)) + (b * c))) + (e * (f - c)) by Lm10
.= (((a * d) + (- (b * d))) + (b * c)) + ((- (a * f)) + (e * (f - c))) by Lm10
.= ((a * d) + ((- (b * d)) + (b * c))) + ((- (a * f)) + (e * (f - c))) by RLVECT_1:def_3
.= ((a * d) + ((b * c) - (b * d))) + ((- (a * f)) + (e * (f - c))) by RLVECT_1:def_11
.= ((a * d) + (b * (c - d))) + ((- (a * f)) + (e * (f - c))) by VECTSP_1:11
.= (- ((- (a * d)) + (- (b * (c - d))))) + ((- (a * f)) + (e * (f - c))) by Lm12
.= (- ((- (a * d)) + (- (b * (c - d))))) + (- ((- (- (a * f))) + (- (e * (f - c))))) by Lm12
.= (- ((- (a * d)) + (- (b * (c - d))))) + (- ((a * f) + (- (e * (f - c))))) by RLVECT_1:17
.= - (((- (a * d)) + (- (b * (c - d)))) + ((a * f) + (- (e * (f - c))))) by RLVECT_1:31
.= - (((- (a * d)) + (- (b * (c - d)))) + (- ((- (a * f)) + (- (- (e * (f - c))))))) by Lm12
.= - (((- (a * d)) + (- (b * (c - d)))) - ((- (a * f)) + (- (- (e * (f - c)))))) by RLVECT_1:def_11
.= - (((- (a * d)) + (- (b * (c - d)))) - ((- (a * f)) + (- ((- (f - c)) * e)))) by VECTSP_1:9
.= - (((- (a * d)) + (- (b * (c - d)))) - ((- (a * f)) + (- (e * (c - f))))) by Lm1
.= - (0. F) by A1, A2, Lm11
.= 0. F by RLVECT_1:12 ;
::_thesis: verum
end;

Lm14:  for F being Field
for a, b, c being Element of F holds a - ((a + b) + (- c)) = c - b
proof
let F be Field; ::_thesis: for a, b, c being Element of F holds a - ((a + b) + (- c)) = c - b
let a, b, c be Element of F; ::_thesis: a - ((a + b) + (- c)) = c - b
thus a - ((a + b) + (- c)) = a - (a + (b + (- c))) by RLVECT_1:def_3
.= a - (a + (b - c)) by RLVECT_1:def_11
.= a + (- (a + (b - c))) by RLVECT_1:def_11
.= a + ((- a) + (- (b - c))) by RLVECT_1:31
.= (a + (- a)) + (- (b - c)) by RLVECT_1:def_3
.= (0. F) + (- (b - c)) by RLVECT_1:def_10
.= - (b - c) by RLVECT_1:4
.= c - b by Lm1 ; ::_thesis: verum
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
let F be Field; ::_thesis: 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
let a, b, c, h, g, e be Element of F; ::_thesis: ((a - b) * (c - ((c + h) + (- g)))) - ((e - ((e + b) + (- a))) * (g - h)) = 0. F
 ( c - ((c + h) + (- g)) = g - h & e - ((e + b) + (- a)) = a - b ) by Lm14;
hence  ((a - b) * (c - ((c + h) + (- g)))) - ((e - ((e + b) + (- a))) * (g - h)) = 0. F by RLVECT_1:15; ::_thesis: verum
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
deffunc H2( Element of H1(F), Element of H1(F)) ->  Element of [: the carrier of F, the carrier of F, the carrier of F:] = [(($1 `1_3) + ($2 `1_3)),(($1 `2_3) + ($2 `2_3)),(($1 `3_3) + ($2 `3_3))];
consider f being BinOp of H1(F) such that
A1: for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds f . (x,y) = H2(x,y) from BINOP_1:sch_4();
take  f ; ::_thesis: for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds f . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))]
thus  for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds f . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] by A1; ::_thesis: verum
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
let f, g be BinOp of H1(F); ::_thesis: ( ( for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds f . (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 g . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] ) implies f = g )
assume that
A2: for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds f . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] and
A3: for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds g . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] ; ::_thesis: f = g
 for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds f . (x,y) = g . (x,y)
proof
let x, y be Element of [: the carrier of F, the carrier of F, the carrier of F:]; ::_thesis: f . (x,y) = g . (x,y)
thus f . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] by A2
.= g . (x,y) by A3 ; ::_thesis: verum
end;
hence  f = g by BINOP_1:2; ::_thesis: verum
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:];
funcx + 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
let F be Field; ::_thesis: for a, b, c, f, g, h being Element of F holds [a,b,c] + [f,g,h] = [(a + f),(b + g),(c + h)]
let a, b, c, f, g, h be Element of F; ::_thesis: [a,b,c] + [f,g,h] = [(a + f),(b + g),(c + h)]
set abc = [a,b,c];
set fgh = [f,g,h];
A1: ( [a,b,c] `3_3 = c & [f,g,h] `1_3 = f ) by MCART_1:def_5, MCART_1:def_7;
A2: ( [f,g,h] `2_3 = g & [f,g,h] `3_3 = h ) by MCART_1:def_6, MCART_1:def_7;
 ( [a,b,c] `1_3 = a & [a,b,c] `2_3 = b ) by MCART_1:def_5, MCART_1:def_6;
hence  [a,b,c] + [f,g,h] = [(a + f),(b + g),(c + h)] by A1, A2, Def1; ::_thesis: verum
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
deffunc H2( Element of H1(F)) ->  Element of [: the carrier of F, the carrier of F, the carrier of F:] = [(- ($1 `1_3)),(- ($1 `2_3)),(- ($1 `3_3))];
consider f being UnOp of H1(F) such that
A1: for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds f . x = H2(x) from FUNCT_2:sch_4();
take  f ; ::_thesis: for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds f . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))]
thus  for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds f . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))] by A1; ::_thesis: verum
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
let f, g be UnOp of H1(F); ::_thesis: ( ( for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds f . 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 g . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))] ) implies f = g )
assume that
A2: for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds f . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))] and
A3: for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds g . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))] ; ::_thesis: f = g
 for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds f . x = g . x
proof
let x be Element of [: the carrier of F, the carrier of F, the carrier of F:]; ::_thesis: f . x = g . x
thus f . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))] by A2
.= g . x by A3 ; ::_thesis: verum
end;
hence  f = g by FUNCT_2:63; ::_thesis: verum
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
attrc1 is strict ;
struct ParStr  ->  1-sorted ;
aggrParStr(# 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
set A = the non empty set ;
set R = the Relation4 of the non empty set ;
take  ParStr(# the non empty set , the Relation4 of the non empty set #) ; ::_thesis: not ParStr(# the non empty set , the Relation4 of the non empty set #) is empty
thus  not the carrier of ParStr(# the non empty set , the Relation4 of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;


definition
let PS be non empty ParStr ;
let a, b, c, d be Element of PS;
preda,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
defpred S1[ set ] means  ex a, b, c, d being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( $1 = [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 );
thus  ex X being set st
for x being set holds
( x in X iff ( x in 4C_3 F & S1[x] ) ) from XBOOLE_0:sch_1(); ::_thesis: verum
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
defpred S1[ set ] means ( $1 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
( $1 = [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 ) );
let H1, H2 be set ; ::_thesis: ( ( for x being set holds
( x in H1 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 H2 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 ) ) ) ) implies H1 = H2 )
assume that
A1: for x being set holds
( x in H1 iff S1[x] ) and
A2: for x being set holds
( x in H2 iff S1[x] ) ; ::_thesis: H1 = H2
 for x being set holds
( x in H1 iff x in H2 )
proof
let x be set ; ::_thesis: ( x in H1 iff x in H2 )
 ( x in H1 iff S1[x] ) by A1;
hence  ( x in H1 iff x in H2 ) by A2; ::_thesis: verum
end;
hence  H1 = H2 by TARSKI:1; ::_thesis: verum
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
let F be Field; ::_thesis: PRs F c= [:(C_3 F),(C_3 F),(C_3 F),(C_3 F):]
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in PRs F or x in [:(C_3 F),(C_3 F),(C_3 F),(C_3 F):] )
 4C_3 F = [:(C_3 F),(C_3 F),(C_3 F),(C_3 F):] ;
hence  ( not x in PRs F or x in [:(C_3 F),(C_3 F),(C_3 F),(C_3 F):] ) by Def9; ::_thesis: verum
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
 PRs F c= [:(C_3 F),(C_3 F),(C_3 F),(C_3 F):] by Th4;
hence  PRs F is Relation4 of C_3 F by Def5; ::_thesis: verum
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
let F be Field; ::_thesis: 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 ) ) )
let a, b, c, d be Element of (MPS F); ::_thesis: ( 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 ) ) )
 ( a,b '||' c,d iff [a,b,c,d] in PR F ) by Def6;
hence  ( 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 Def9; ::_thesis: verum
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
let F be Field; ::_thesis: 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 ) )
let a, b, c, d be Element of (MPS F); ::_thesis: ( 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 ) )
 [a,b,c,d] in 4C_3 F ;
hence  ( 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 ) ) by Th9; ::_thesis: verum
end;

theorem Th13: :: PARSP_1:13
for F being Field
for a, b being Element of (MPS F) holds a,b '||' b,a
proof
let F be Field; ::_thesis: for a, b being Element of (MPS F) holds a,b '||' b,a
let a, b be Element of (MPS F); ::_thesis: a,b '||' b,a
consider e, f being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A1: [e,f,f,e] = [a,b,b,a] ;
A2: (((e `2_3) - (f `2_3)) * ((f `3_3) - (e `3_3))) - (((f `2_3) - (e `2_3)) * ((e `3_3) - (f `3_3))) = 0. F by Lm2;
 ( (((e `1_3) - (f `1_3)) * ((f `2_3) - (e `2_3))) - (((f `1_3) - (e `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((f `3_3) - (e `3_3))) - (((f `1_3) - (e `1_3)) * ((e `3_3) - (f `3_3))) = 0. F ) by Lm2;
hence  a,b '||' b,a by A1, A2, Th12; ::_thesis: verum
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
let F be Field; ::_thesis: for a, b, c being Element of (MPS F) holds a,b '||' c,c
let a, b, c be Element of (MPS F); ::_thesis: a,b '||' c,c
consider e, f, g being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A1: [e,f,g,g] = [a,b,c,c] ;
A2: (((e `2_3) - (f `2_3)) * ((g `3_3) - (g `3_3))) - (((g `2_3) - (g `2_3)) * ((e `3_3) - (f `3_3))) = 0. F by Lm3;
 ( (((e `1_3) - (f `1_3)) * ((g `2_3) - (g `2_3))) - (((g `1_3) - (g `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (g `3_3))) - (((g `1_3) - (g `1_3)) * ((e `3_3) - (f `3_3))) = 0. F ) by Lm3;
hence  a,b '||' c,c by A1, A2, Th12; ::_thesis: verum
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
let F be Field; ::_thesis: 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
let a, b, p, q, r, s be Element of (MPS F); ::_thesis: ( a,b '||' p,q & a,b '||' r,s & not p,q '||' r,s implies a = b )
defpred S1[ Element of H1(F), Element of H1(F), Element of H1(F), Element of H1(F)] means ( ((($1 `1_3) - ($2 `1_3)) * (($3 `2_3) - ($4 `2_3))) - ((($3 `1_3) - ($4 `1_3)) * (($1 `2_3) - ($2 `2_3))) = 0. F & ((($1 `1_3) - ($2 `1_3)) * (($3 `3_3) - ($4 `3_3))) - ((($3 `1_3) - ($4 `1_3)) * (($1 `3_3) - ($2 `3_3))) = 0. F & ((($1 `2_3) - ($2 `2_3)) * (($3 `3_3) - ($4 `3_3))) - ((($3 `2_3) - ($4 `2_3)) * (($1 `3_3) - ($2 `3_3))) = 0. F );
assume that
A1: a,b '||' p,q and
A2: a,b '||' r,s ; ::_thesis: ( p,q '||' r,s or a = b )
consider e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A3: [e,f,g,h] = [a,b,p,q] and
A4: S1[e,f,g,h] by A1, Th12;
consider i, j, k, l being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A5: [i,j,k,l] = [a,b,r,s] and
A6: S1[i,j,k,l] by A2, Th12;
A7: ( i = a & j = b ) by A5, XTUPLE_0:5;
A8: ( k = r & l = s ) by A5, XTUPLE_0:5;
set A = (e `1_3) - (f `1_3);
set B = (e `2_3) - (f `2_3);
set C = (e `3_3) - (f `3_3);
set D = (g `1_3) - (h `1_3);
set E = (g `2_3) - (h `2_3);
set K = (g `3_3) - (h `3_3);
set G = (k `1_3) - (l `1_3);
set H = (k `2_3) - (l `2_3);
set I = (k `3_3) - (l `3_3);
A9: ( e = a & f = b ) by A3, XTUPLE_0:5;
A10: ( g = p & h = q ) by A3, XTUPLE_0:5;
now__::_thesis:_(_a_<>_b_implies_ex_g,_h,_k,_l_being_Element_of_[:_the_carrier_of_F,_the_carrier_of_F,_the_carrier_of_F:]_st_
(_[g,h,k,l]_=_[p,q,r,s]_&_S1[g,h,k,l]_)_)
assume A11: a <> b ; ::_thesis: ex g, h, k, l being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( [g,h,k,l] = [p,q,r,s] & S1[g,h,k,l] )
now__::_thesis:_(_(_(e_`1_3)_-_(f_`1_3)_<>_0._F_&_(((g_`1_3)_-_(h_`1_3))_*_((k_`2_3)_-_(l_`2_3)))_-_(((k_`1_3)_-_(l_`1_3))_*_((g_`2_3)_-_(h_`2_3)))_=_0._F_&_(((g_`1_3)_-_(h_`1_3))_*_((k_`3_3)_-_(l_`3_3)))_-_(((k_`1_3)_-_(l_`1_3))_*_((g_`3_3)_-_(h_`3_3)))_=_0._F_&_(((g_`2_3)_-_(h_`2_3))_*_((k_`3_3)_-_(l_`3_3)))_-_(((k_`2_3)_-_(l_`2_3))_*_((g_`3_3)_-_(h_`3_3)))_=_0._F_)_or_(_(e_`2_3)_-_(f_`2_3)_<>_0._F_&_(((g_`1_3)_-_(h_`1_3))_*_((k_`2_3)_-_(l_`2_3)))_-_(((k_`1_3)_-_(l_`1_3))_*_((g_`2_3)_-_(h_`2_3)))_=_0._F_&_(((g_`2_3)_-_(h_`2_3))_*_((k_`3_3)_-_(l_`3_3)))_-_(((k_`2_3)_-_(l_`2_3))_*_((g_`3_3)_-_(h_`3_3)))_=_0._F_&_(((g_`1_3)_-_(h_`1_3))_*_((k_`3_3)_-_(l_`3_3)))_-_(((k_`1_3)_-_(l_`1_3))_*_((g_`3_3)_-_(h_`3_3)))_=_0._F_)_or_(_(e_`3_3)_-_(f_`3_3)_<>_0._F_&_(((g_`2_3)_-_(h_`2_3))_*_((k_`3_3)_-_(l_`3_3)))_-_(((k_`2_3)_-_(l_`2_3))_*_((g_`3_3)_-_(h_`3_3)))_=_0._F_&_(((g_`1_3)_-_(h_`1_3))_*_((k_`2_3)_-_(l_`2_3)))_-_(((k_`1_3)_-_(l_`1_3))_*_((g_`2_3)_-_(h_`2_3)))_=_0._F_&_(((g_`1_3)_-_(h_`1_3))_*_((k_`3_3)_-_(l_`3_3)))_-_(((k_`1_3)_-_(l_`1_3))_*_((g_`3_3)_-_(h_`3_3)))_=_0._F_)_)
 e = [(e `1_3),(e `2_3),(e `3_3)] by MCART_1:44;
then A12: ( e `1_3 <> f `1_3 or e `2_3 <> f `2_3 or e `3_3 <> f `3_3 ) by A9, A11, MCART_1:44;
percases ( (e `1_3) - (f `1_3) <> 0. F or (e `2_3) - (f `2_3) <> 0. F or (e `3_3) - (f `3_3) <> 0. F ) by A12, RLVECT_1:21;
caseA13: (e `1_3) - (f `1_3) <> 0. F ; ::_thesis: ( (((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F & (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F )
hence  (((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3))) = 0. F by A4, A6, A9, A7, Lm4; ::_thesis: ( (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F & (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F )
thus A14: (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F by A4, A6, A9, A7, A13, Lm4; ::_thesis: (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F
 ( ((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3)) = ((((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) * (((e `1_3) - (f `1_3)) ")) * ((k `3_3) - (l `3_3)) & ((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3)) = ((((k `1_3) - (l `1_3)) * ((e `2_3) - (f `2_3))) * (((e `1_3) - (f `1_3)) ")) * ((g `3_3) - (h `3_3)) ) by A4, A6, A9, A7, A13, VECTSP_1:30;
hence  (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F by A14, Lm8; ::_thesis: verum
end;
caseA15: (e `2_3) - (f `2_3) <> 0. F ; ::_thesis: ( (((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3))) = 0. F & (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F )
hence  (((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3))) = 0. F by A4, A6, A9, A7, Lm6; ::_thesis: ( (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F )
thus A16: (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F by A4, A6, A9, A7, A15, Lm4; ::_thesis: (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F
 ( ((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3)) = ((((g `2_3) - (h `2_3)) * ((e `1_3) - (f `1_3))) * (((e `2_3) - (f `2_3)) ")) * ((k `3_3) - (l `3_3)) & ((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3)) = ((((k `2_3) - (l `2_3)) * ((e `1_3) - (f `1_3))) * (((e `2_3) - (f `2_3)) ")) * ((g `3_3) - (h `3_3)) ) by A4, A6, A9, A7, A15, VECTSP_1:30;
hence  (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F by A16, Lm8; ::_thesis: verum
end;
caseA17: (e `3_3) - (f `3_3) <> 0. F ; ::_thesis: ( (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F )
hence  (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F by A4, A6, A9, A7, Lm6; ::_thesis: ( (((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F )
A18: ( ((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3)) = ((((g `3_3) - (h `3_3)) * ((e `1_3) - (f `1_3))) * (((e `3_3) - (f `3_3)) ")) * ((k `2_3) - (l `2_3)) & ((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3)) = ((((k `3_3) - (l `3_3)) * ((e `1_3) - (f `1_3))) * (((e `3_3) - (f `3_3)) ")) * ((g `2_3) - (h `2_3)) ) by A4, A6, A9, A7, A17, VECTSP_1:30;
 (((g `3_3) - (h `3_3)) * ((k `2_3) - (l `2_3))) - (((k `3_3) - (l `3_3)) * ((g `2_3) - (h `2_3))) = 0. F by A4, A6, A9, A7, A17, Lm6;
hence  (((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3))) = 0. F by A18, Lm8; ::_thesis: (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F
thus  (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F by A4, A6, A9, A7, A17, Lm6; ::_thesis: verum
end;
end;
end;
hence  ex g, h, k, l being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( [g,h,k,l] = [p,q,r,s] & S1[g,h,k,l] ) by A10, A8; ::_thesis: verum
end;
hence  ( p,q '||' r,s or a = b ) by Th12; ::_thesis: verum
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
let F be Field; ::_thesis: for a, b, c being Element of (MPS F) st a,b '||' a,c holds
b,a '||' b,c
let a, b, c be Element of (MPS F); ::_thesis: ( a,b '||' a,c implies b,a '||' b,c )
assume  a,b '||' a,c ; ::_thesis: b,a '||' b,c
then consider e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A1: [e,f,g,h] = [a,b,a,c] and
A2: ( (((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 ) and
A3: (((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 Th12;
A4: e = a by A1, XTUPLE_0:5;
A5: g = a by A1, XTUPLE_0:5;
then A6: (((f `2_3) - (e `2_3)) * ((f `3_3) - (h `3_3))) - (((f `2_3) - (h `2_3)) * ((f `3_3) - (e `3_3))) = 0. F by A3, A4, Lm13;
 f = b by A1, XTUPLE_0:5;
then A7: [f,e,f,h] = [b,a,b,c] by A1, A4, XTUPLE_0:5;
 ( (((f `1_3) - (e `1_3)) * ((f `2_3) - (h `2_3))) - (((f `1_3) - (h `1_3)) * ((f `2_3) - (e `2_3))) = 0. F & (((f `1_3) - (e `1_3)) * ((f `3_3) - (h `3_3))) - (((f `1_3) - (h `1_3)) * ((f `3_3) - (e `3_3))) = 0. F ) by A2, A4, A5, Lm13;
hence  b,a '||' b,c by A7, A6, Th12; ::_thesis: verum
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
let F be Field; ::_thesis: 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 )
let a, b, c be Element of (MPS F); ::_thesis: ex d being Element of (MPS F) st
( a,b '||' c,d & a,c '||' b,d )
consider e, f, g being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A1: ( e = a & f = b & g = c ) ;
set h = (g + f) + (- e);
reconsider d = (g + f) + (- e) as Element of (MPS F) ;
A2: [e,f,g,((g + f) + (- e))] = [a,b,c,d] by A1;
take  d ; ::_thesis: ( a,b '||' c,d & a,c '||' b,d )
 ( g + f = [((g `1_3) + (f `1_3)),((g `2_3) + (f `2_3)),((g `3_3) + (f `3_3))] & - e = [(- (e `1_3)),(- (e `2_3)),(- (e `3_3))] ) by Def1, Def3;
then A3: (g + f) + (- e) = [(((g `1_3) + (f `1_3)) + (- (e `1_3))),(((g `2_3) + (f `2_3)) + (- (e `2_3))),(((g `3_3) + (f `3_3)) + (- (e `3_3)))] by Th2;
then A4: ((g + f) + (- e)) `1_3 = ((g `1_3) + (f `1_3)) + (- (e `1_3)) by MCART_1:def_5;
A5: ((g + f) + (- e)) `3_3 = ((g `3_3) + (f `3_3)) + (- (e `3_3)) by A3, MCART_1:def_7;
then A6: (((e `1_3) - (f `1_3)) * ((g `3_3) - (((g + f) + (- e)) `3_3))) - (((g `1_3) - (((g + f) + (- e)) `1_3)) * ((e `3_3) - (f `3_3))) = 0. F by A4, Lm15;
A7: (((e `1_3) - (g `1_3)) * ((f `3_3) - (((g + f) + (- e)) `3_3))) - (((f `1_3) - (((g + f) + (- e)) `1_3)) * ((e `3_3) - (g `3_3))) = 0. F by A4, A5, Lm15;
A8: ((g + f) + (- e)) `2_3 = ((g `2_3) + (f `2_3)) + (- (e `2_3)) by A3, MCART_1:def_6;
then A9: (((e `2_3) - (f `2_3)) * ((g `3_3) - (((g + f) + (- e)) `3_3))) - (((g `2_3) - (((g + f) + (- e)) `2_3)) * ((e `3_3) - (f `3_3))) = 0. F by A5, Lm15;
 (((e `1_3) - (f `1_3)) * ((g `2_3) - (((g + f) + (- e)) `2_3))) - (((g `1_3) - (((g + f) + (- e)) `1_3)) * ((e `2_3) - (f `2_3))) = 0. F by A4, A8, Lm15;
hence  a,b '||' c,d by A2, A6, A9, Th12; ::_thesis: a,c '||' b,d
A10: [e,g,f,((g + f) + (- e))] = [a,c,b,d] by A1;
A11: (((e `2_3) - (g `2_3)) * ((f `3_3) - (((g + f) + (- e)) `3_3))) - (((f `2_3) - (((g + f) + (- e)) `2_3)) * ((e `3_3) - (g `3_3))) = 0. F by A8, A5, Lm15;
 (((e `1_3) - (g `1_3)) * ((f `2_3) - (((g + f) + (- e)) `2_3))) - (((f `1_3) - (((g + f) + (- e)) `1_3)) * ((e `2_3) - (g `2_3))) = 0. F by A4, A8, Lm15;
hence  a,c '||' b,d by A10, A7, A11, Th12; ::_thesis: verum
end;

definition
let IT be non empty ParStr ;
attrIT 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
set F = the Field;
 for a, b, c, d, p, q, r, s being Element of (MPS the Field) 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 (MPS the Field) st
( a,b '||' c,x & a,c '||' b,x ) ) by Th13, Th14, Th15, Th16, Th17;
then  MPS the Field is ParSp-like by Def12;
hence  ex b1 being non empty ParStr st
( b1 is strict & b1 is ParSp-like ) ; ::_thesis: verum
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
let PS be ParSp; ::_thesis: for a, b being Element of PS holds a,b '||' a,b
let a, b be Element of PS; ::_thesis: a,b '||' a,b
 b,a '||' b,b by Def12;
hence  a,b '||' a,b by Def12; ::_thesis: verum
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
let PS be ParSp; ::_thesis: for a, b, c, d being Element of PS st a,b '||' c,d holds
c,d '||' a,b
let a, b, c, d be Element of PS; ::_thesis: ( a,b '||' c,d implies c,d '||' a,b )
assume A1: a,b '||' c,d ; ::_thesis: c,d '||' a,b
 a,b '||' a,b by Th18;
then  ( a <> b implies c,d '||' a,b ) by A1, Def12;
hence  c,d '||' a,b by Def12; ::_thesis: verum
end;

theorem Th20: :: PARSP_1:20
for PS being ParSp
for a, b, c being Element of PS holds a,a '||' b,c
proof
let PS be ParSp; ::_thesis: for a, b, c being Element of PS holds a,a '||' b,c
let a, b, c be Element of PS; ::_thesis: a,a '||' b,c
 b,c '||' a,a by Def12;
hence  a,a '||' b,c by Th19; ::_thesis: verum
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
let PS be ParSp; ::_thesis: for a, b, c, d being Element of PS st a,b '||' c,d holds
b,a '||' c,d
let a, b, c, d be Element of PS; ::_thesis: ( a,b '||' c,d implies b,a '||' c,d )
assume A1: a,b '||' c,d ; ::_thesis: b,a '||' c,d
 a,b '||' b,a by Def12;
then  ( a <> b implies b,a '||' c,d ) by A1, Def12;
hence  b,a '||' c,d by A1; ::_thesis: verum
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
let PS be ParSp; ::_thesis: for a, b, c, d being Element of PS st a,b '||' c,d holds
a,b '||' d,c
let a, b, c, d be Element of PS; ::_thesis: ( a,b '||' c,d implies a,b '||' d,c )
assume  a,b '||' c,d ; ::_thesis: a,b '||' d,c
then  c,d '||' a,b by Th19;
then  d,c '||' a,b by Th21;
hence  a,b '||' d,c by Th19; ::_thesis: verum
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
let PS be ParSp; ::_thesis: 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 )
let a, b, c, d be Element of PS; ::_thesis: ( a,b '||' c,d implies ( 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 ) )
assume  a,b '||' c,d ; ::_thesis: ( 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 )
then  c,d '||' a,b by Th19;
then A1: d,c '||' a,b by Th21;
then A2: d,c '||' b,a by Th22;
then  c,d '||' b,a by Th21;
hence  ( 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 ) by A1, A2, Th19, Th21; ::_thesis: verum
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
let PS be ParSp; ::_thesis: 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 )
let a, b, c be Element of PS; ::_thesis: ( a,b '||' a,c implies ( 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 ) )
assume A1: a,b '||' a,c ; ::_thesis: ( 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 )
then  a,c '||' a,b by Th19;
then A2: c,a '||' c,b by Def12;
 b,a '||' b,c by A1, Def12;
hence  ( 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 ) by A1, A2, Th23; ::_thesis: verum
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
let PS be ParSp; ::_thesis: 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
let a, b, p, q, r, s be Element of PS; ::_thesis: ( a <> b & p,q '||' a,b & a,b '||' r,s implies p,q '||' r,s )
assume that
A1: a <> b and
A2: p,q '||' a,b and
A3: a,b '||' r,s ; ::_thesis: p,q '||' r,s
 a,b '||' p,q by A2, Th23;
hence  p,q '||' r,s by A1, A3, Def12; ::_thesis: verum
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
let PS be ParSp; ::_thesis: 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 )
let a, b, c be Element of PS; ::_thesis: ( not a,b '||' a,c implies ( 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 ) )
assume A1: not a,b '||' a,c ; ::_thesis: ( 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 )
assume  ( a,c '||' a,b or b,a '||' a,c or a,b '||' c,a or a,c '||' b,a or b,a '||' c,a or c,a '||' a,b or c,a '||' b,a or b,a '||' b,c or a,b '||' b,c or b,a '||' c,b or b,c '||' b,a or b,a '||' c,b or c,b '||' b,a or b,c '||' a,b or c,b '||' a,b or c,a '||' c,b or a,c '||' c,b or c,a '||' b,c or a,c '||' b,c or c,b '||' c,a or b,c '||' c,a or c,b '||' a,c or b,c '||' a,c ) ; ::_thesis: contradiction
then  ( a,c '||' a,b or a,b '||' a,c or a,b '||' a,c or a,c '||' a,b or a,b '||' a,c or a,c '||' a,b or a,c '||' a,b or b,a '||' b,c or b,a '||' b,c or b,a '||' b,c or b,c '||' b,a or b,a '||' b,c or b,c '||' b,a or b,c '||' b,a or b,c '||' b,a or c,a '||' c,b or c,a '||' c,b or c,a '||' c,b or c,a '||' c,b or c,b '||' c,a or c,b '||' c,a or c,b '||' c,a or c,b '||' c,a ) by Th23;
hence  contradiction by A1, Th24; ::_thesis: verum
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
let PS be ParSp; ::_thesis: 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
let a, b, c, d, p, q, r, s be Element of PS; ::_thesis: ( not a,b '||' c,d & a,b '||' p,q & c,d '||' r,s & p <> q & r <> s implies not p,q '||' r,s )
assume that
A1: not a,b '||' c,d and
A2: a,b '||' p,q and
A3: c,d '||' r,s and
A4: p <> q and
A5: r <> s ; ::_thesis: not p,q '||' r,s
assume  p,q '||' r,s ; ::_thesis: contradiction
then  a,b '||' r,s by A2, A4, Th26;
then A6: r,s '||' a,b by Th23;
 r,s '||' c,d by A3, Th23;
hence  contradiction by A1, A5, A6, Def12; ::_thesis: verum
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
let PS be ParSp; ::_thesis: 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
let a, b, c, p, q, r be Element of PS; ::_thesis: ( not a,b '||' a,c & a,b '||' p,q & a,c '||' p,r & b,c '||' q,r & p <> q implies not p,q '||' p,r )
assume that
A1: not a,b '||' a,c and
A2: a,b '||' p,q and
A3: a,c '||' p,r and
A4: b,c '||' q,r and
A5: p <> q ; ::_thesis: not p,q '||' p,r
now__::_thesis:_not_p_=_r
assume  p = r ; ::_thesis: contradiction
then A6: p,q '||' b,c by A4, Th23;
 p,q '||' b,a by A2, Th23;
then  b,a '||' b,c by A5, A6, Def12;
hence  contradiction by A1, Th24; ::_thesis: verum
end;
hence  not p,q '||' p,r by A1, A2, A3, A5, Th30; ::_thesis: verum
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
let PS be ParSp; ::_thesis: 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
let a, b, c, p, r be Element of PS; ::_thesis: ( not a,b '||' a,c & a,c '||' p,r & b,c '||' p,r implies p = r )
assume that
A1: ( not a,b '||' a,c & a,c '||' p,r ) and
A2: b,c '||' p,r ; ::_thesis: p = r
A3: p,r '||' b,c by A2, Th23;
 ( not a,c '||' b,c & p,r '||' a,c ) by A1, Th23, Th29;
hence  p = r by A3, Def12; ::_thesis: verum
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
let PS be ParSp; ::_thesis: 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
let p, q, r, s be Element of PS; ::_thesis: ( not p,q '||' p,r & p,r '||' p,s & q,r '||' q,s implies r = s )
assume that
A1: ( not p,q '||' p,r & p,r '||' p,s ) and
A2: q,r '||' q,s ; ::_thesis: r = s
A3: r,s '||' r,q by A2, Th29;
 ( not r,p '||' r,q & r,s '||' r,p ) by A1, Th29;
hence  r = s by A3, Def12; ::_thesis: verum
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
let PS be ParSp; ::_thesis: 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
let a, b, c, p, q, r, s be Element of PS; ::_thesis: ( 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 implies r = s )
assume that
A1: not a,b '||' a,c and
A2: a,b '||' p,q and
A3: a,c '||' p,r and
A4: a,c '||' p,s and
A5: b,c '||' q,r and
A6: b,c '||' q,s ; ::_thesis: r = s
A7: now__::_thesis:_(_p_<>_q_implies_r_=_s_)
 b <> c by A1, Th18;
then A8: q,r '||' q,s by A5, A6, Def12;
 a <> c by A1, Def12;
then A9: p,r '||' p,s by A3, A4, Def12;
assume  p <> q ; ::_thesis: r = s
then  not p,q '||' p,r by A1, A2, A3, A5, Th31;
hence  r = s by A9, A8, Th33; ::_thesis: verum
end;
 ( p = q implies ( p = r & p = s ) ) by A1, A3, A4, A5, A6, Th32;
hence  r = s by A7; ::_thesis: verum
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
let PS be ParSp; ::_thesis: for a, b, c, d being Element of PS st a,b '||' a,c & a,b '||' a,d holds
a,b '||' c,d
let a, b, c, d be Element of PS; ::_thesis: ( a,b '||' a,c & a,b '||' a,d implies a,b '||' c,d )
assume that
A1: a,b '||' a,c and
A2: a,b '||' a,d ; ::_thesis: a,b '||' c,d
now__::_thesis:_(_a_<>_b_&_a_<>_c_implies_a,b_'||'_c,d_)
assume that
A3: a <> b and
A4: a <> c ; ::_thesis: a,b '||' c,d
 a,c '||' a,d by A1, A2, A3, Def12;
then  a,c '||' c,d by Th24;
hence  a,b '||' c,d by A1, A4, Th26; ::_thesis: verum
end;
hence  a,b '||' c,d by A2, Th20; ::_thesis: verum
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
let PS be ParSp; ::_thesis: ( ( for a, b being Element of PS holds a = b ) implies for p, q, r, s being Element of PS holds p,q '||' r,s )
assume A1: for a, b being Element of PS holds a = b ; ::_thesis: for p, q, r, s being Element of PS holds p,q '||' r,s
let p, q, r, s be Element of PS; ::_thesis: p,q '||' r,s
 r = s by A1;
hence  p,q '||' r,s by Def12; ::_thesis: verum
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
let PS be ParSp; ::_thesis: ( ex a, b being Element of PS st
( a <> b & ( for c being Element of PS holds a,b '||' a,c ) ) implies for p, q, r, s being Element of PS holds p,q '||' r,s )
assume  ex a, b being Element of PS st
( a <> b & ( for c being Element of PS holds a,b '||' a,c ) ) ; ::_thesis: for p, q, r, s being Element of PS holds p,q '||' r,s
then consider a, b being Element of PS such that
A1: a <> b and
A2: for c being Element of PS holds a,b '||' a,c ;
let p, q, r, s be Element of PS; ::_thesis: p,q '||' r,s
 ( a,b '||' a,r & a,b '||' a,s ) by A2;
then A3: a,b '||' r,s by Th35;
 ( a,b '||' a,p & a,b '||' a,q ) by A2;
then  a,b '||' p,q by Th35;
hence  p,q '||' r,s by A1, A3, Def12; ::_thesis: verum
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
let PS be ParSp; ::_thesis: 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
let a, b, c, p, q be Element of PS; ::_thesis: ( not a,b '||' a,c & p <> q & p,q '||' p,a & p,q '||' p,b implies not p,q '||' p,c )
assume that
A1: not a,b '||' a,c and
A2: p <> q ; ::_thesis: ( not p,q '||' p,a or not p,q '||' p,b or not p,q '||' p,c )
assume A3: ( p,q '||' p,a & p,q '||' p,b & p,q '||' p,c ) ; ::_thesis: contradiction
then  p,a '||' p,b by A2, Def12;
then A4: a,p '||' a,b by Th24;
 p,a '||' p,c by A2, A3, Def12;
then A5: a,p '||' a,c by Th24;
 a <> p by A1, A2, A3, Def12;
hence  contradiction by A1, A4, A5, Def12; ::_thesis: verum
end;