:: PARSP_2 semantic presentation

begin

Lm1:  for F being non empty right_complementable add-associative right_zeroed addLoopStr
for a, b being Element of F st a - b = 0. F holds
a = b
proof
let F be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for a, b being Element of F st a - b = 0. F holds
a = b
let a, b be Element of F; ::_thesis: ( a - b = 0. F implies a = b )
assume  a - b = 0. F ; ::_thesis: a = b
then  a + (- b) = 0. F by RLVECT_1:def_11;
then  a = - (- b) by RLVECT_1:6;
hence  a = b by RLVECT_1:17; ::_thesis: verum
end;

Lm2:  for F being non empty right_complementable add-associative right_zeroed addLoopStr
for x, y being Element of F holds
( ( x + (- y) = 0. F implies x = y ) & ( x = y implies x + (- y) = 0. F ) & ( x - y = 0. F implies x = y ) & ( x = y implies x - y = 0. F ) )
proof
let F be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for x, y being Element of F holds
( ( x + (- y) = 0. F implies x = y ) & ( x = y implies x + (- y) = 0. F ) & ( x - y = 0. F implies x = y ) & ( x = y implies x - y = 0. F ) )
let x, y be Element of F; ::_thesis: ( ( x + (- y) = 0. F implies x = y ) & ( x = y implies x + (- y) = 0. F ) & ( x - y = 0. F implies x = y ) & ( x = y implies x - y = 0. F ) )
A1: ( x + (- y) = 0. F implies x = y )
proof
assume  x + (- y) = 0. F ; ::_thesis: x = y
then  x + ((- y) + y) = (0. F) + y by RLVECT_1:def_3;
then  x + (0. F) = (0. F) + y by RLVECT_1:5;
then  x = (0. F) + y by RLVECT_1:4;
hence  x = y by RLVECT_1:4; ::_thesis: verum
end;
A2: ( x - y = 0. F implies x = y )
proof
assume  x - y = 0. F ; ::_thesis: x = y
then  (x + (- y)) + y = (0. F) + y by RLVECT_1:def_11;
then  x + ((- y) + y) = (0. F) + y by RLVECT_1:def_3;
then  x + (0. F) = (0. F) + y by RLVECT_1:5;
then  x = (0. F) + y by RLVECT_1:4;
hence  x = y by RLVECT_1:4; ::_thesis: verum
end;
 ( x = y implies x - y = 0. F )
proof
assume  x = y ; ::_thesis: x - y = 0. F
then  x - y = y + (- y) by RLVECT_1:def_11;
hence  x - y = 0. F by RLVECT_1:5; ::_thesis: verum
end;
hence  ( ( x + (- y) = 0. F implies x = y ) & ( x = y implies x + (- y) = 0. F ) & ( x - y = 0. F implies x = y ) & ( x = y implies x - y = 0. F ) ) by A1, A2, RLVECT_1:5; ::_thesis: verum
end;

theorem Th1: :: PARSP_2:1
for F being Field holds MPS F is ParSp
proof
let F be Field; ::_thesis: MPS F is ParSp
 for a, b, c, d, p, q, r, s being Element of (MPS F) 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 F) st
( a,b '||' c,x & a,c '||' b,x ) ) by PARSP_1:13, PARSP_1:14, PARSP_1:15, PARSP_1:16, PARSP_1:17;
hence  MPS F is ParSp by PARSP_1:def_12; ::_thesis: verum
end;

                         Lm3:  for F being Field
for e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds
( ( (((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 ) iff ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) )
proof
let F be Field; ::_thesis: for e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds
( ( (((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 ) iff ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) )
let e, f, g, h be Element of [: the carrier of F, the carrier of F, the carrier of F:]; ::_thesis: ( ( (((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 ) iff ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) )
A1: ( (((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 K being Element of F holds
( not K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) or not K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) or not K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) ) implies ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) )
proof
assume that
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 and
A3: (((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
A4: (((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 ; ::_thesis: ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) )
now__::_thesis:_(_ex_K_being_Element_of_F_st_
(_K_*_((e_`1_3)_-_(f_`1_3))_=_(g_`1_3)_-_(h_`1_3)_&_K_*_((e_`2_3)_-_(f_`2_3))_=_(g_`2_3)_-_(h_`2_3)_&_K_*_((e_`3_3)_-_(f_`3_3))_=_(g_`3_3)_-_(h_`3_3)_)_or_(_(e_`1_3)_-_(f_`1_3)_=_0._F_&_(e_`2_3)_-_(f_`2_3)_=_0._F_&_(e_`3_3)_-_(f_`3_3)_=_0._F_)_)
A5: now__::_thesis:_(_(e_`3_3)_-_(f_`3_3)_<>_0._F_&_(_for_K_being_Element_of_F_holds_
(_not_K_*_((e_`1_3)_-_(f_`1_3))_=_(g_`1_3)_-_(h_`1_3)_or_not_K_*_((e_`2_3)_-_(f_`2_3))_=_(g_`2_3)_-_(h_`2_3)_or_not_K_*_((e_`3_3)_-_(f_`3_3))_=_(g_`3_3)_-_(h_`3_3)_)_)_implies_(_(e_`1_3)_-_(f_`1_3)_=_0._F_&_(e_`2_3)_-_(f_`2_3)_=_0._F_&_(e_`3_3)_-_(f_`3_3)_=_0._F_)_)
assume A6: (e `3_3) - (f `3_3) <> 0. F ; ::_thesis: ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) )
A7: (((g `3_3) - (h `3_3)) * (((e `3_3) - (f `3_3)) ")) * ((e `3_3) - (f `3_3)) = ((g `3_3) - (h `3_3)) * ((((e `3_3) - (f `3_3)) ") * ((e `3_3) - (f `3_3))) by GROUP_1:def_3
.= ((g `3_3) - (h `3_3)) * (1_ F) by A6, VECTSP_1:def_10
.= (g `3_3) - (h `3_3) by VECTSP_1:def_8 ;
A8: (((g `3_3) - (h `3_3)) * (((e `3_3) - (f `3_3)) ")) * ((e `2_3) - (f `2_3)) = (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) * (((e `3_3) - (f `3_3)) ") by GROUP_1:def_3
.= (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) * (((e `3_3) - (f `3_3)) ") by A4, Lm1
.= ((g `2_3) - (h `2_3)) * (((e `3_3) - (f `3_3)) * (((e `3_3) - (f `3_3)) ")) by GROUP_1:def_3
.= ((g `2_3) - (h `2_3)) * (1_ F) by A6, VECTSP_1:def_10
.= (g `2_3) - (h `2_3) by VECTSP_1:def_8 ;
(((g `3_3) - (h `3_3)) * (((e `3_3) - (f `3_3)) ")) * ((e `1_3) - (f `1_3)) = (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) * (((e `3_3) - (f `3_3)) ") by GROUP_1:def_3
.= (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) * (((e `3_3) - (f `3_3)) ") by A3, Lm1
.= ((g `1_3) - (h `1_3)) * (((e `3_3) - (f `3_3)) * (((e `3_3) - (f `3_3)) ")) by GROUP_1:def_3
.= ((g `1_3) - (h `1_3)) * (1_ F) by A6, VECTSP_1:def_10
.= (g `1_3) - (h `1_3) by VECTSP_1:def_8 ;
hence  ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) by A8, A7; ::_thesis: verum
end;
A9: now__::_thesis:_(_(e_`2_3)_-_(f_`2_3)_<>_0._F_&_(_for_K_being_Element_of_F_holds_
(_not_K_*_((e_`1_3)_-_(f_`1_3))_=_(g_`1_3)_-_(h_`1_3)_or_not_K_*_((e_`2_3)_-_(f_`2_3))_=_(g_`2_3)_-_(h_`2_3)_or_not_K_*_((e_`3_3)_-_(f_`3_3))_=_(g_`3_3)_-_(h_`3_3)_)_)_implies_(_(e_`1_3)_-_(f_`1_3)_=_0._F_&_(e_`2_3)_-_(f_`2_3)_=_0._F_&_(e_`3_3)_-_(f_`3_3)_=_0._F_)_)
assume A10: (e `2_3) - (f `2_3) <> 0. F ; ::_thesis: ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) )
A11: (((g `2_3) - (h `2_3)) * (((e `2_3) - (f `2_3)) ")) * ((e `2_3) - (f `2_3)) = ((g `2_3) - (h `2_3)) * ((((e `2_3) - (f `2_3)) ") * ((e `2_3) - (f `2_3))) by GROUP_1:def_3
.= ((g `2_3) - (h `2_3)) * (1_ F) by A10, VECTSP_1:def_10
.= (g `2_3) - (h `2_3) by VECTSP_1:def_8 ;
A12: (((g `2_3) - (h `2_3)) * (((e `2_3) - (f `2_3)) ")) * ((e `3_3) - (f `3_3)) = (((e `2_3) - (f `2_3)) ") * (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) by GROUP_1:def_3
.= (((e `2_3) - (f `2_3)) ") * (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) by A4, Lm1
.= ((((e `2_3) - (f `2_3)) ") * ((e `2_3) - (f `2_3))) * ((g `3_3) - (h `3_3)) by GROUP_1:def_3
.= ((g `3_3) - (h `3_3)) * (1_ F) by A10, VECTSP_1:def_10
.= (g `3_3) - (h `3_3) by VECTSP_1:def_8 ;
(((g `2_3) - (h `2_3)) * (((e `2_3) - (f `2_3)) ")) * ((e `1_3) - (f `1_3)) = (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) * (((e `2_3) - (f `2_3)) ") by GROUP_1:def_3
.= (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) * (((e `2_3) - (f `2_3)) ") by A2, Lm1
.= ((g `1_3) - (h `1_3)) * (((e `2_3) - (f `2_3)) * (((e `2_3) - (f `2_3)) ")) by GROUP_1:def_3
.= ((g `1_3) - (h `1_3)) * (1_ F) by A10, VECTSP_1:def_10
.= (g `1_3) - (h `1_3) by VECTSP_1:def_8 ;
hence  ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) by A11, A12; ::_thesis: verum
end;
now__::_thesis:_(_(e_`1_3)_-_(f_`1_3)_<>_0._F_&_(_for_K_being_Element_of_F_holds_
(_not_K_*_((e_`1_3)_-_(f_`1_3))_=_(g_`1_3)_-_(h_`1_3)_or_not_K_*_((e_`2_3)_-_(f_`2_3))_=_(g_`2_3)_-_(h_`2_3)_or_not_K_*_((e_`3_3)_-_(f_`3_3))_=_(g_`3_3)_-_(h_`3_3)_)_)_implies_(_(e_`1_3)_-_(f_`1_3)_=_0._F_&_(e_`2_3)_-_(f_`2_3)_=_0._F_&_(e_`3_3)_-_(f_`3_3)_=_0._F_)_)
assume A13: (e `1_3) - (f `1_3) <> 0. F ; ::_thesis: ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) )
A14: (((g `1_3) - (h `1_3)) * (((e `1_3) - (f `1_3)) ")) * ((e `1_3) - (f `1_3)) = ((g `1_3) - (h `1_3)) * ((((e `1_3) - (f `1_3)) ") * ((e `1_3) - (f `1_3))) by GROUP_1:def_3
.= ((g `1_3) - (h `1_3)) * (1_ F) by A13, VECTSP_1:def_10
.= (g `1_3) - (h `1_3) by VECTSP_1:def_8 ;
A15: (((g `1_3) - (h `1_3)) * (((e `1_3) - (f `1_3)) ")) * ((e `3_3) - (f `3_3)) = (((e `1_3) - (f `1_3)) ") * (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) by GROUP_1:def_3
.= (((e `1_3) - (f `1_3)) ") * (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) by A3, Lm1
.= ((((e `1_3) - (f `1_3)) ") * ((e `1_3) - (f `1_3))) * ((g `3_3) - (h `3_3)) by GROUP_1:def_3
.= ((g `3_3) - (h `3_3)) * (1_ F) by A13, VECTSP_1:def_10
.= (g `3_3) - (h `3_3) by VECTSP_1:def_8 ;
(((g `1_3) - (h `1_3)) * (((e `1_3) - (f `1_3)) ")) * ((e `2_3) - (f `2_3)) = (((e `1_3) - (f `1_3)) ") * (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) by GROUP_1:def_3
.= (((e `1_3) - (f `1_3)) ") * (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) by A2, Lm1
.= ((((e `1_3) - (f `1_3)) ") * ((e `1_3) - (f `1_3))) * ((g `2_3) - (h `2_3)) by GROUP_1:def_3
.= ((g `2_3) - (h `2_3)) * (1_ F) by A13, VECTSP_1:def_10
.= (g `2_3) - (h `2_3) by VECTSP_1:def_8 ;
hence  ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) by A14, A15; ::_thesis: verum
end;
hence  ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) by A9, A5; ::_thesis: verum
end;
hence  ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) ; ::_thesis: verum
end;
 ( ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) implies ( (((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
A16: now__::_thesis:_(_ex_K_being_Element_of_F_st_
(_K_*_((e_`1_3)_-_(f_`1_3))_=_(g_`1_3)_-_(h_`1_3)_&_K_*_((e_`2_3)_-_(f_`2_3))_=_(g_`2_3)_-_(h_`2_3)_&_K_*_((e_`3_3)_-_(f_`3_3))_=_(g_`3_3)_-_(h_`3_3)_)_&_(_ex_K_being_Element_of_F_st_
(_K_*_((e_`1_3)_-_(f_`1_3))_=_(g_`1_3)_-_(h_`1_3)_&_K_*_((e_`2_3)_-_(f_`2_3))_=_(g_`2_3)_-_(h_`2_3)_&_K_*_((e_`3_3)_-_(f_`3_3))_=_(g_`3_3)_-_(h_`3_3)_)_or_(_(e_`1_3)_-_(f_`1_3)_=_0._F_&_(e_`2_3)_-_(f_`2_3)_=_0._F_&_(e_`3_3)_-_(f_`3_3)_=_0._F_)_)_implies_(_(((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_)_)
given K being Element of F such that A17: K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) and
A18: ( K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) ; ::_thesis: ( ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) implies ( (((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 ) )
A19: (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = ((K * ((e `2_3) - (f `2_3))) * ((e `3_3) - (f `3_3))) - ((K * ((e `2_3) - (f `2_3))) * ((e `3_3) - (f `3_3))) by A18, GROUP_1:def_3;
 ( (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = ((K * ((e `1_3) - (f `1_3))) * ((e `2_3) - (f `2_3))) - ((K * ((e `1_3) - (f `1_3))) * ((e `2_3) - (f `2_3))) & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = ((K * ((e `1_3) - (f `1_3))) * ((e `3_3) - (f `3_3))) - ((K * ((e `1_3) - (f `1_3))) * ((e `3_3) - (f `3_3))) ) by A17, A18, GROUP_1:def_3;
hence  ( ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) implies ( (((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 A19, RLVECT_1:15; ::_thesis: verum
end;
A20: now__::_thesis:_(_(e_`1_3)_-_(f_`1_3)_=_0._F_&_(e_`2_3)_-_(f_`2_3)_=_0._F_&_(e_`3_3)_-_(f_`3_3)_=_0._F_&_(_ex_K_being_Element_of_F_st_
(_K_*_((e_`1_3)_-_(f_`1_3))_=_(g_`1_3)_-_(h_`1_3)_&_K_*_((e_`2_3)_-_(f_`2_3))_=_(g_`2_3)_-_(h_`2_3)_&_K_*_((e_`3_3)_-_(f_`3_3))_=_(g_`3_3)_-_(h_`3_3)_)_or_(_(e_`1_3)_-_(f_`1_3)_=_0._F_&_(e_`2_3)_-_(f_`2_3)_=_0._F_&_(e_`3_3)_-_(f_`3_3)_=_0._F_)_)_implies_(_(((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_)_)
assume that
A21: (e `1_3) - (f `1_3) = 0. F and
A22: (e `2_3) - (f `2_3) = 0. F and
A23: (e `3_3) - (f `3_3) = 0. F ; ::_thesis: ( ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) implies ( (((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 ) )
A24: ((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3)) = 0. F by A23, VECTSP_1:7;
 ( ((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3)) = 0. F & ((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3)) = 0. F ) by A21, VECTSP_1:7;
hence  ( ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) implies ( (((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 A21, A22, A24, RLVECT_1:15; ::_thesis: verum
end;
assume  ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) ; ::_thesis: ( (((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 )
hence  ( (((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 A20, A16; ::_thesis: verum
end;
hence  ( ( (((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 ) iff ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) ) by A1; ::_thesis: verum
end;

theorem Th2: :: PARSP_2:2
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] & ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (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] & ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (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] & ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) ) )
A1: ( a,b '||' c,d implies 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] & ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) ) )
proof
assume  a,b '||' c,d ; ::_thesis: 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] & ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) )
then consider e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A2: [a,b,c,d] = [e,f,g,h] and
A3: ( (((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 PARSP_1:12;
 ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) by A3, Lm3;
hence  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] & ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) ) by A2; ::_thesis: verum
end;
 ( 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] & ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) ) implies a,b '||' c,d )
proof
given e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that A4: [a,b,c,d] = [e,f,g,h] and
A5: ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) ; ::_thesis: a,b '||' c,d
A6: (((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 A5, Lm3;
 ( (((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 ) by A5, Lm3;
hence  a,b '||' c,d by A4, A6, PARSP_1:12; ::_thesis: verum
end;
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] & ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) ) ) by A1; ::_thesis: verum
end;

theorem Th3: :: PARSP_2:3
for F being Field
for a, b, c being Element of (MPS F)
for e, f, g being Element of [: the carrier of F, the carrier of F, the carrier of F:] st not a,b '||' a,c & [a,b,a,c] = [e,f,e,g] holds
( e <> f & e <> g & f <> g )
proof
let F be Field; ::_thesis: for a, b, c being Element of (MPS F)
for e, f, g being Element of [: the carrier of F, the carrier of F, the carrier of F:] st not a,b '||' a,c & [a,b,a,c] = [e,f,e,g] holds
( e <> f & e <> g & f <> g )
let a, b, c be Element of (MPS F); ::_thesis: for e, f, g being Element of [: the carrier of F, the carrier of F, the carrier of F:] st not a,b '||' a,c & [a,b,a,c] = [e,f,e,g] holds
( e <> f & e <> g & f <> g )
let e, f, g be Element of [: the carrier of F, the carrier of F, the carrier of F:]; ::_thesis: ( not a,b '||' a,c & [a,b,a,c] = [e,f,e,g] implies ( e <> f & e <> g & f <> g ) )
assume A1: ( not a,b '||' a,c & [a,b,a,c] = [e,f,e,g] ) ; ::_thesis: ( e <> f & e <> g & f <> g )
then  ( (0. F) * ((e `1_3) - (f `1_3)) <> (e `1_3) - (g `1_3) or (0. F) * ((e `2_3) - (f `2_3)) <> (e `2_3) - (g `2_3) or (0. F) * ((e `3_3) - (f `3_3)) <> (e `3_3) - (g `3_3) ) by Th2;
then A2: ( 0. F <> (e `1_3) - (g `1_3) or 0. F <> (e `2_3) - (g `2_3) or 0. F <> (e `3_3) - (g `3_3) ) by VECTSP_1:12;
A3: f <> g
proof
assume A4: not f <> g ; ::_thesis: contradiction
 ( ((e `1_3) - (f `1_3)) * (1_ F) <> (e `1_3) - (g `1_3) or ((e `2_3) - (f `2_3)) * (1_ F) <> (e `2_3) - (g `2_3) or ((e `3_3) - (f `3_3)) * (1_ F) <> (e `3_3) - (g `3_3) ) by A1, Th2;
hence  contradiction by A4, VECTSP_1:def_8; ::_thesis: verum
end;
 ( (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 A1, Th2;
hence  ( e <> f & e <> g & f <> g ) by A2, A3, RLVECT_1:15; ::_thesis: verum
end;

theorem Th4: :: PARSP_2:4
for F being Field
for a, b, c being Element of (MPS F)
for e, f, g being Element of [: the carrier of F, the carrier of F, the carrier of F:]
for K, L being Element of F st not a,b '||' a,c & [a,b,a,c] = [e,f,e,g] & K * ((e `1_3) - (f `1_3)) = L * ((e `1_3) - (g `1_3)) & K * ((e `2_3) - (f `2_3)) = L * ((e `2_3) - (g `2_3)) & K * ((e `3_3) - (f `3_3)) = L * ((e `3_3) - (g `3_3)) holds
( K = 0. F & L = 0. F )
proof
let F be Field; ::_thesis: for a, b, c being Element of (MPS F)
for e, f, g being Element of [: the carrier of F, the carrier of F, the carrier of F:]
for K, L being Element of F st not a,b '||' a,c & [a,b,a,c] = [e,f,e,g] & K * ((e `1_3) - (f `1_3)) = L * ((e `1_3) - (g `1_3)) & K * ((e `2_3) - (f `2_3)) = L * ((e `2_3) - (g `2_3)) & K * ((e `3_3) - (f `3_3)) = L * ((e `3_3) - (g `3_3)) holds
( K = 0. F & L = 0. F )
let a, b, c be Element of (MPS F); ::_thesis: for e, f, g being Element of [: the carrier of F, the carrier of F, the carrier of F:]
for K, L being Element of F st not a,b '||' a,c & [a,b,a,c] = [e,f,e,g] & K * ((e `1_3) - (f `1_3)) = L * ((e `1_3) - (g `1_3)) & K * ((e `2_3) - (f `2_3)) = L * ((e `2_3) - (g `2_3)) & K * ((e `3_3) - (f `3_3)) = L * ((e `3_3) - (g `3_3)) holds
( K = 0. F & L = 0. F )
let e, f, g be Element of [: the carrier of F, the carrier of F, the carrier of F:]; ::_thesis: for K, L being Element of F st not a,b '||' a,c & [a,b,a,c] = [e,f,e,g] & K * ((e `1_3) - (f `1_3)) = L * ((e `1_3) - (g `1_3)) & K * ((e `2_3) - (f `2_3)) = L * ((e `2_3) - (g `2_3)) & K * ((e `3_3) - (f `3_3)) = L * ((e `3_3) - (g `3_3)) holds
( K = 0. F & L = 0. F )
let K, L be Element of F; ::_thesis: ( not a,b '||' a,c & [a,b,a,c] = [e,f,e,g] & K * ((e `1_3) - (f `1_3)) = L * ((e `1_3) - (g `1_3)) & K * ((e `2_3) - (f `2_3)) = L * ((e `2_3) - (g `2_3)) & K * ((e `3_3) - (f `3_3)) = L * ((e `3_3) - (g `3_3)) implies ( K = 0. F & L = 0. F ) )
assume that
A1: ( not a,b '||' a,c & [a,b,a,c] = [e,f,e,g] ) and
A2: K * ((e `1_3) - (f `1_3)) = L * ((e `1_3) - (g `1_3)) and
A3: K * ((e `2_3) - (f `2_3)) = L * ((e `2_3) - (g `2_3)) and
A4: K * ((e `3_3) - (f `3_3)) = L * ((e `3_3) - (g `3_3)) ; ::_thesis: ( K = 0. F & L = 0. F )
 ( e = [(e `1_3),(e `2_3),(e `3_3)] & g = [(g `1_3),(g `2_3),(g `3_3)] ) by MCART_1:44;
then  ( e `1_3 <> g `1_3 or e `2_3 <> g `2_3 or e `3_3 <> g `3_3 ) by A1, Th3;
then A5: ( (e `1_3) - (g `1_3) <> 0. F or (e `2_3) - (g `2_3) <> 0. F or (e `3_3) - (g `3_3) <> 0. F ) by Lm2;
 ( (K * ((e `1_3) - (f `1_3))) * ((e `2_3) - (g `2_3)) = L * (((e `1_3) - (g `1_3)) * ((e `2_3) - (g `2_3))) & (K * ((e `2_3) - (f `2_3))) * ((e `1_3) - (g `1_3)) = L * (((e `2_3) - (g `2_3)) * ((e `1_3) - (g `1_3))) ) by A2, A3, GROUP_1:def_3;
then  ((K * ((e `1_3) - (f `1_3))) * ((e `2_3) - (g `2_3))) - ((K * ((e `2_3) - (f `2_3))) * ((e `1_3) - (g `1_3))) = 0. F by RLVECT_1:15;
then  (K * (((e `1_3) - (f `1_3)) * ((e `2_3) - (g `2_3)))) - ((K * ((e `2_3) - (f `2_3))) * ((e `1_3) - (g `1_3))) = 0. F by GROUP_1:def_3;
then  (K * (((e `1_3) - (f `1_3)) * ((e `2_3) - (g `2_3)))) - (K * (((e `2_3) - (f `2_3)) * ((e `1_3) - (g `1_3)))) = 0. F by GROUP_1:def_3;
then A6: K * ((((e `1_3) - (f `1_3)) * ((e `2_3) - (g `2_3))) - (((e `1_3) - (g `1_3)) * ((e `2_3) - (f `2_3)))) = 0. F by VECTSP_1:11;
 ( (K * ((e `1_3) - (f `1_3))) * ((e `3_3) - (g `3_3)) = L * (((e `1_3) - (g `1_3)) * ((e `3_3) - (g `3_3))) & (K * ((e `3_3) - (f `3_3))) * ((e `1_3) - (g `1_3)) = L * (((e `3_3) - (g `3_3)) * ((e `1_3) - (g `1_3))) ) by A2, A4, GROUP_1:def_3;
then  ((K * ((e `1_3) - (f `1_3))) * ((e `3_3) - (g `3_3))) - ((K * ((e `3_3) - (f `3_3))) * ((e `1_3) - (g `1_3))) = 0. F by RLVECT_1:15;
then  (K * (((e `1_3) - (f `1_3)) * ((e `3_3) - (g `3_3)))) - ((K * ((e `3_3) - (f `3_3))) * ((e `1_3) - (g `1_3))) = 0. F by GROUP_1:def_3;
then  (K * (((e `1_3) - (f `1_3)) * ((e `3_3) - (g `3_3)))) - (K * (((e `3_3) - (f `3_3)) * ((e `1_3) - (g `1_3)))) = 0. F by GROUP_1:def_3;
then A7: K * ((((e `1_3) - (f `1_3)) * ((e `3_3) - (g `3_3))) - (((e `1_3) - (g `1_3)) * ((e `3_3) - (f `3_3)))) = 0. F by VECTSP_1:11;
 ( (K * ((e `2_3) - (f `2_3))) * ((e `3_3) - (g `3_3)) = L * (((e `2_3) - (g `2_3)) * ((e `3_3) - (g `3_3))) & (K * ((e `3_3) - (f `3_3))) * ((e `2_3) - (g `2_3)) = L * (((e `3_3) - (g `3_3)) * ((e `2_3) - (g `2_3))) ) by A3, A4, GROUP_1:def_3;
then  ((K * ((e `2_3) - (f `2_3))) * ((e `3_3) - (g `3_3))) - ((K * ((e `3_3) - (f `3_3))) * ((e `2_3) - (g `2_3))) = 0. F by RLVECT_1:15;
then  (K * (((e `2_3) - (f `2_3)) * ((e `3_3) - (g `3_3)))) - ((K * ((e `3_3) - (f `3_3))) * ((e `2_3) - (g `2_3))) = 0. F by GROUP_1:def_3;
then  (K * (((e `2_3) - (f `2_3)) * ((e `3_3) - (g `3_3)))) - (K * (((e `3_3) - (f `3_3)) * ((e `2_3) - (g `2_3)))) = 0. F by GROUP_1:def_3;
then A8: K * ((((e `2_3) - (f `2_3)) * ((e `3_3) - (g `3_3))) - (((e `2_3) - (g `2_3)) * ((e `3_3) - (f `3_3)))) = 0. F by VECTSP_1:11;
A9: ( (((e `1_3) - (f `1_3)) * ((e `2_3) - (g `2_3))) - (((e `1_3) - (g `1_3)) * ((e `2_3) - (f `2_3))) <> 0. F or (((e `2_3) - (f `2_3)) * ((e `3_3) - (g `3_3))) - (((e `2_3) - (g `2_3)) * ((e `3_3) - (f `3_3))) <> 0. F or (((e `1_3) - (f `1_3)) * ((e `3_3) - (g `3_3))) - (((e `1_3) - (g `1_3)) * ((e `3_3) - (f `3_3))) <> 0. F ) by A1, PARSP_1:12;
then A10: K = 0. F by A6, A8, A7, VECTSP_1:12;
then A11: 0. F = L * ((e `3_3) - (g `3_3)) by A4, VECTSP_1:7;
 ( 0. F = L * ((e `1_3) - (g `1_3)) & 0. F = L * ((e `2_3) - (g `2_3)) ) by A2, A3, A10, VECTSP_1:7;
hence  ( K = 0. F & L = 0. F ) by A6, A8, A7, A9, A11, A5, VECTSP_1:12; ::_thesis: verum
end;

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

Lm5:  for F being Field
for K, L, R being Element of F holds (K - L) - (R - L) = K - R
proof
let F be Field; ::_thesis: for K, L, R being Element of F holds (K - L) - (R - L) = K - R
let K, L, R be Element of F; ::_thesis: (K - L) - (R - L) = K - R
thus (K - L) - (R - L) = (K + (- L)) - (R - L) by RLVECT_1:def_11
.= ((- L) + K) - (R + (- L)) by RLVECT_1:def_11
.= K - R by Lm4 ; ::_thesis: verum
end;

Lm6:  for F being Field
for K, N, M, L, S being Element of F st (K * (N - M)) - (L * (N - S)) = S - M holds
(K + (- (1_ F))) * (N - M) = (L + (- (1_ F))) * (N - S)
proof
let F be Field; ::_thesis: for K, N, M, L, S being Element of F st (K * (N - M)) - (L * (N - S)) = S - M holds
(K + (- (1_ F))) * (N - M) = (L + (- (1_ F))) * (N - S)
let K, N, M, L, S be Element of F; ::_thesis: ( (K * (N - M)) - (L * (N - S)) = S - M implies (K + (- (1_ F))) * (N - M) = (L + (- (1_ F))) * (N - S) )
assume  (K * (N - M)) - (L * (N - S)) = S - M ; ::_thesis: (K + (- (1_ F))) * (N - M) = (L + (- (1_ F))) * (N - S)
then (K * (N - M)) - (L * (N - S)) = S + (- M) by RLVECT_1:def_11
.= (S + (- M)) + (0. F) by RLVECT_1:4
.= ((- M) + S) + ((- N) + N) by RLVECT_1:5
.= S + (((- N) + N) + (- M)) by RLVECT_1:def_3
.= S + ((- N) + (N + (- M))) by RLVECT_1:def_3
.= S + ((- N) + (N - M)) by RLVECT_1:def_11
.= (S + (- N)) + (N - M) by RLVECT_1:def_3
.= (S - N) + (N - M) by RLVECT_1:def_11 ;
then  ((K * (N - M)) + (- (L * (N - S)))) + (L * (N - S)) = ((S - N) + (N - M)) + (L * (N - S)) by RLVECT_1:def_11;
then  (K * (N - M)) + ((- (L * (N - S))) + (L * (N - S))) = ((S - N) + (N - M)) + (L * (N - S)) by RLVECT_1:def_3;
then  (K * (N - M)) + (0. F) = ((S - N) + (N - M)) + (L * (N - S)) by RLVECT_1:5;
then K * (N - M) = ((S - N) + (N - M)) + (L * (N - S)) by RLVECT_1:4
.= ((S - N) + (L * (N - S))) + (N - M) by RLVECT_1:def_3 ;
then (K * (N - M)) + (- (N - M)) = ((S - N) + (L * (N - S))) + ((N - M) + (- (N - M))) by RLVECT_1:def_3
.= ((S - N) + (L * (N - S))) + (0. F) by RLVECT_1:5
.= (S - N) + (L * (N - S)) by RLVECT_1:4
.= (S + (- N)) + (L * (N - S)) by RLVECT_1:def_11
.= (L * (N - S)) + (- (N - S)) by RLVECT_1:33 ;
then  (K * (N - M)) + (- ((1_ F) * (N - M))) = (L * (N - S)) + (- (N - S)) by VECTSP_1:def_8;
then  (K * (N - M)) + ((- (1_ F)) * (N - M)) = (L * (N - S)) + (- (N - S)) by VECTSP_1:9;
then (K + (- (1_ F))) * (N - M) = (L * (N - S)) + (- (N - S)) by VECTSP_1:def_7
.= (L * (N - S)) + (- ((1_ F) * (N - S))) by VECTSP_1:def_8
.= (L * (N - S)) + ((- (1_ F)) * (N - S)) by VECTSP_1:9 ;
hence  (K + (- (1_ F))) * (N - M) = (L + (- (1_ F))) * (N - S) by VECTSP_1:def_7; ::_thesis: verum
end;

Lm7:  for F being Field
for K, L, N, M being Element of F st K - L = N - M holds
M = (L + N) - K
proof
let F be Field; ::_thesis: for K, L, N, M being Element of F st K - L = N - M holds
M = (L + N) - K
let K, L, N, M be Element of F; ::_thesis: ( K - L = N - M implies M = (L + N) - K )
assume  K - L = N - M ; ::_thesis: M = (L + N) - K
then  M + (K + (- L)) = M + (N - M) by RLVECT_1:def_11;
then  M + (K + (- L)) = M + (N + (- M)) by RLVECT_1:def_11;
then  (M + K) + (- L) = M + (N + (- M)) by RLVECT_1:def_3;
then  (M + K) + (- L) = (M + N) + (- M) by RLVECT_1:def_3;
then  (M + K) - L = (N + M) + (- M) by RLVECT_1:def_11;
then  (M + K) - L = N + (M + (- M)) by RLVECT_1:def_3;
then  (M + K) - L = N + (0. F) by RLVECT_1:5;
then  ((M + K) - L) + L = N + L by RLVECT_1:4;
then  ((M + K) + (- L)) + L = N + L by RLVECT_1:def_11;
then  (M + K) + ((- L) + L) = N + L by RLVECT_1:def_3;
then  (M + K) + (0. F) = L + N by RLVECT_1:5;
then  (M + K) + (- K) = (L + N) + (- K) by RLVECT_1:4;
then  (M + K) + (- K) = (L + N) - K by RLVECT_1:def_11;
then  M + (K + (- K)) = (L + N) - K by RLVECT_1:def_3;
then  M + (0. F) = (L + N) - K by RLVECT_1:5;
hence  M = (L + N) - K by RLVECT_1:4; ::_thesis: verum
end;

theorem Th5: :: PARSP_2:5
for F being Field
for a, b, c, d being Element of (MPS F)
for e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] st not a,b '||' a,c & a,b '||' c,d & a,c '||' b,d & [a,b,c,d] = [e,f,g,h] holds
( h `1_3 = ((f `1_3) + (g `1_3)) - (e `1_3) & h `2_3 = ((f `2_3) + (g `2_3)) - (e `2_3) & h `3_3 = ((f `3_3) + (g `3_3)) - (e `3_3) )
proof
let F be Field; ::_thesis: for a, b, c, d being Element of (MPS F)
for e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] st not a,b '||' a,c & a,b '||' c,d & a,c '||' b,d & [a,b,c,d] = [e,f,g,h] holds
( h `1_3 = ((f `1_3) + (g `1_3)) - (e `1_3) & h `2_3 = ((f `2_3) + (g `2_3)) - (e `2_3) & h `3_3 = ((f `3_3) + (g `3_3)) - (e `3_3) )
let a, b, c, d be Element of (MPS F); ::_thesis: for e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] st not a,b '||' a,c & a,b '||' c,d & a,c '||' b,d & [a,b,c,d] = [e,f,g,h] holds
( h `1_3 = ((f `1_3) + (g `1_3)) - (e `1_3) & h `2_3 = ((f `2_3) + (g `2_3)) - (e `2_3) & h `3_3 = ((f `3_3) + (g `3_3)) - (e `3_3) )
let e, f, g, h be Element of [: the carrier of F, the carrier of F, the carrier of F:]; ::_thesis: ( not a,b '||' a,c & a,b '||' c,d & a,c '||' b,d & [a,b,c,d] = [e,f,g,h] implies ( h `1_3 = ((f `1_3) + (g `1_3)) - (e `1_3) & h `2_3 = ((f `2_3) + (g `2_3)) - (e `2_3) & h `3_3 = ((f `3_3) + (g `3_3)) - (e `3_3) ) )
assume that
A1: not a,b '||' a,c and
A2: a,b '||' c,d and
A3: a,c '||' b,d and
A4: [a,b,c,d] = [e,f,g,h] ; ::_thesis: ( h `1_3 = ((f `1_3) + (g `1_3)) - (e `1_3) & h `2_3 = ((f `2_3) + (g `2_3)) - (e `2_3) & h `3_3 = ((f `3_3) + (g `3_3)) - (e `3_3) )
A5: e = [(e `1_3),(e `2_3),(e `3_3)] by MCART_1:44;
consider m, n, o, w being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A6: [a,c,b,d] = [m,n,o,w] and
A7: ( ex L being Element of F st
( L * ((m `1_3) - (n `1_3)) = (o `1_3) - (w `1_3) & L * ((m `2_3) - (n `2_3)) = (o `2_3) - (w `2_3) & L * ((m `3_3) - (n `3_3)) = (o `3_3) - (w `3_3) ) or ( (m `1_3) - (n `1_3) = 0. F & (m `2_3) - (n `2_3) = 0. F & (m `3_3) - (n `3_3) = 0. F ) ) by A3, Th2;
A8: b = f by A4, XTUPLE_0:5;
then A9: o = f by A6, XTUPLE_0:5;
 d = h by A4, XTUPLE_0:5;
then A10: w = h by A6, XTUPLE_0:5;
 c = g by A4, XTUPLE_0:5;
then A11: n = g by A6, XTUPLE_0:5;
A12: a = e by A4, XTUPLE_0:5;
then A13: [a,b,a,c] = [e,f,e,g] by A4, A8, XTUPLE_0:5;
consider i, j, k, l being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A14: [a,b,c,d] = [i,j,k,l] and
A15: ( ex K being Element of F st
( K * ((i `1_3) - (j `1_3)) = (k `1_3) - (l `1_3) & K * ((i `2_3) - (j `2_3)) = (k `2_3) - (l `2_3) & K * ((i `3_3) - (j `3_3)) = (k `3_3) - (l `3_3) ) or ( (i `1_3) - (j `1_3) = 0. F & (i `2_3) - (j `2_3) = 0. F & (i `3_3) - (j `3_3) = 0. F ) ) by A2, Th2;
A16: ( e = i & f = j ) by A4, A14, XTUPLE_0:5;
A17: ( g = k & h = l ) by A4, A14, XTUPLE_0:5;
A18: e = m by A12, A6, XTUPLE_0:5;
 f = [(f `1_3),(f `2_3),(f `3_3)] by MCART_1:44;
then  ( e `1_3 <> f `1_3 or e `2_3 <> f `2_3 or e `3_3 <> f `3_3 ) by A1, A13, A5, Th3;
then consider K being Element of F such that
A19: K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) and
A20: K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) and
A21: K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) by A15, A16, A17, Lm2;
 g = [(g `1_3),(g `2_3),(g `3_3)] by MCART_1:44;
then  ( e `1_3 <> g `1_3 or e `2_3 <> g `2_3 or e `3_3 <> g `3_3 ) by A1, A13, A5, Th3;
then consider L being Element of F such that
A22: L * ((e `1_3) - (g `1_3)) = (f `1_3) - (h `1_3) and
A23: L * ((e `2_3) - (g `2_3)) = (f `2_3) - (h `2_3) and
A24: L * ((e `3_3) - (g `3_3)) = (f `3_3) - (h `3_3) by A7, A18, A11, A9, A10, Lm2;
 (K * ((e `2_3) - (f `2_3))) - (L * ((e `2_3) - (g `2_3))) = (g `2_3) - (f `2_3) by A20, A23, Lm5;
then A25: (K + (- (1_ F))) * ((e `2_3) - (f `2_3)) = (L + (- (1_ F))) * ((e `2_3) - (g `2_3)) by Lm6;
 (K * ((e `3_3) - (f `3_3))) - (L * ((e `3_3) - (g `3_3))) = (g `3_3) - (f `3_3) by A21, A24, Lm5;
then A26: (K + (- (1_ F))) * ((e `3_3) - (f `3_3)) = (L + (- (1_ F))) * ((e `3_3) - (g `3_3)) by Lm6;
 (K * ((e `1_3) - (f `1_3))) - (L * ((e `1_3) - (g `1_3))) = (g `1_3) - (f `1_3) by A19, A22, Lm5;
then  (K + (- (1_ F))) * ((e `1_3) - (f `1_3)) = (L + (- (1_ F))) * ((e `1_3) - (g `1_3)) by Lm6;
then A27: K + (- (1_ F)) = 0. F by A1, A13, A25, A26, Th4;
then  ((e `2_3) - (f `2_3)) * (1_ F) = (g `2_3) - (h `2_3) by A20, Lm2;
then A28: (e `2_3) - (f `2_3) = (g `2_3) - (h `2_3) by VECTSP_1:def_8;
 ((e `3_3) - (f `3_3)) * (1_ F) = (g `3_3) - (h `3_3) by A21, A27, Lm2;
then A29: (e `3_3) - (f `3_3) = (g `3_3) - (h `3_3) by VECTSP_1:def_8;
 ((e `1_3) - (f `1_3)) * (1_ F) = (g `1_3) - (h `1_3) by A19, A27, Lm2;
then  (e `1_3) - (f `1_3) = (g `1_3) - (h `1_3) by VECTSP_1:def_8;
hence  ( h `1_3 = ((f `1_3) + (g `1_3)) - (e `1_3) & h `2_3 = ((f `2_3) + (g `2_3)) - (e `2_3) & h `3_3 = ((f `3_3) + (g `3_3)) - (e `3_3) ) by A28, A29, Lm7; ::_thesis: verum
end;

Lm8:  for F being Field
for L, K, R being Element of F st (L * K) - (L * R) = R + K holds
(L - (1_ F)) * K = (L + (1_ F)) * R
proof
let F be Field; ::_thesis: for L, K, R being Element of F st (L * K) - (L * R) = R + K holds
(L - (1_ F)) * K = (L + (1_ F)) * R
let L, K, R be Element of F; ::_thesis: ( (L * K) - (L * R) = R + K implies (L - (1_ F)) * K = (L + (1_ F)) * R )
assume  (L * K) - (L * R) = R + K ; ::_thesis: (L - (1_ F)) * K = (L + (1_ F)) * R
then ((L * K) + (- (L * R))) + (- K) = (R + K) + (- K) by RLVECT_1:def_11
.= R + (K + (- K)) by RLVECT_1:def_3
.= R + (0. F) by RLVECT_1:5
.= R by RLVECT_1:4 ;
then  ((L * K) + (- K)) + (- (L * R)) = R by RLVECT_1:def_3;
then  ((L * K) + (- ((1_ F) * K))) + (- (L * R)) = R by VECTSP_1:def_8;
then  ((L * K) + ((- (1_ F)) * K)) + (- (L * R)) = R by VECTSP_1:9;
then  ((L + (- (1_ F))) * K) + (- (L * R)) = R by VECTSP_1:def_7;
then  (((L - (1_ F)) * K) + (- (L * R))) + (L * R) = R + (L * R) by RLVECT_1:def_11;
then  ((L - (1_ F)) * K) + ((- (L * R)) + (L * R)) = R + (L * R) by RLVECT_1:def_3;
then  ((L - (1_ F)) * K) + (0. F) = R + (L * R) by RLVECT_1:5;
then (L - (1_ F)) * K = (L * R) + R by RLVECT_1:4
.= (L * R) + ((1_ F) * R) by VECTSP_1:def_8 ;
hence  (L - (1_ F)) * K = (L + (1_ F)) * R by VECTSP_1:def_7; ::_thesis: verum
end;

Lm9:  for F being Field
for L, K, N, R, S being Element of F st L * (K - N) = R - S & S = (K + N) - R holds
(L - (1_ F)) * (R - N) = (L + (1_ F)) * (R - K)
proof
let F be Field; ::_thesis: for L, K, N, R, S being Element of F st L * (K - N) = R - S & S = (K + N) - R holds
(L - (1_ F)) * (R - N) = (L + (1_ F)) * (R - K)
let L, K, N, R, S be Element of F; ::_thesis: ( L * (K - N) = R - S & S = (K + N) - R implies (L - (1_ F)) * (R - N) = (L + (1_ F)) * (R - K) )
assume  ( L * (K - N) = R - S & S = (K + N) - R ) ; ::_thesis: (L - (1_ F)) * (R - N) = (L + (1_ F)) * (R - K)
then A1: L * (K - N) = R + (- ((K + N) - R)) by RLVECT_1:def_11
.= R + (R + (- (K + N))) by RLVECT_1:33
.= R + (R + ((- K) + (- N))) by RLVECT_1:31
.= R + ((- N) + (R + (- K))) by RLVECT_1:def_3
.= (R + (- N)) + (R + (- K)) by RLVECT_1:def_3
.= (R - N) + (R + (- K)) by RLVECT_1:def_11
.= (R - K) + (R - N) by RLVECT_1:def_11 ;
(L * (R - N)) - (L * (R - K)) = (L * (R + (- N))) - (L * (R - K)) by RLVECT_1:def_11
.= (L * (R + (- N))) - (L * (R + (- K))) by RLVECT_1:def_11
.= (L * (R + (- N))) + (- (L * (R + (- K)))) by RLVECT_1:def_11
.= ((L * R) + (L * (- N))) + (- (L * (R + (- K)))) by VECTSP_1:def_7
.= ((L * R) + (L * (- N))) + ((- L) * (R + (- K))) by VECTSP_1:9
.= ((L * R) + (L * (- N))) + (((- L) * R) + ((- L) * (- K))) by VECTSP_1:def_7
.= ((L * R) + (L * (- N))) + (((- L) * R) + (L * K)) by VECTSP_1:10
.= ((L * (- N)) + (L * R)) + ((- (L * R)) + (L * K)) by VECTSP_1:9
.= (((L * (- N)) + (L * R)) + (- (L * R))) + (L * K) by RLVECT_1:def_3
.= ((L * (- N)) + ((L * R) + (- (L * R)))) + (L * K) by RLVECT_1:def_3
.= ((L * (- N)) + (0. F)) + (L * K) by RLVECT_1:5
.= (L * K) + (L * (- N)) by RLVECT_1:4
.= L * (K + (- N)) by VECTSP_1:def_7
.= L * (K - N) by RLVECT_1:def_11 ;
hence  (L - (1_ F)) * (R - N) = (L + (1_ F)) * (R - K) by A1, Lm8; ::_thesis: verum
end;

Lm10:  for F being Field
for K, L, M, N, R, S being Element of F st K = (L + M) - N & R = (L + S) - N holds
(1_ F) * (M - S) = K - R
proof
let F be Field; ::_thesis: for K, L, M, N, R, S being Element of F st K = (L + M) - N & R = (L + S) - N holds
(1_ F) * (M - S) = K - R
let K, L, M, N, R, S be Element of F; ::_thesis: ( K = (L + M) - N & R = (L + S) - N implies (1_ F) * (M - S) = K - R )
assume that
A1: K = (L + M) - N and
A2: R = (L + S) - N ; ::_thesis: (1_ F) * (M - S) = K - R
- R = - ((L + S) + (- N)) by A2, RLVECT_1:def_11
.= (- (L + S)) + (- (- N)) by RLVECT_1:31
.= (- (L + S)) + N by RLVECT_1:17
.= ((- L) + (- S)) + N by RLVECT_1:31 ;
then K - R = ((L + M) - N) + (((- L) + (- S)) + N) by A1, RLVECT_1:def_11
.= ((M + L) + (- N)) + (((- L) + (- S)) + N) by RLVECT_1:def_11
.= ((M + L) + (- N)) + ((- S) + ((- L) + N)) by RLVECT_1:def_3
.= (M + (L + (- N))) + ((- S) + ((- L) + N)) by RLVECT_1:def_3
.= (M + (L - N)) + ((- S) + ((- L) + N)) by RLVECT_1:def_11
.= (M + (L - N)) + ((- S) + ((- L) + (- (- N)))) by RLVECT_1:17
.= (M + (L - N)) + ((- S) + (- (L + (- N)))) by RLVECT_1:31
.= (M + (L - N)) + ((- (L - N)) + (- S)) by RLVECT_1:def_11
.= ((M + (L - N)) + (- (L - N))) + (- S) by RLVECT_1:def_3
.= (M + ((L - N) + (- (L - N)))) + (- S) by RLVECT_1:def_3
.= (M + (0. F)) + (- S) by RLVECT_1:5
.= M + (- S) by RLVECT_1:4
.= (M * (1_ F)) + (- S) by VECTSP_1:def_8
.= (M * (1_ F)) + ((- S) * (1_ F)) by VECTSP_1:def_8
.= (M + (- S)) * (1_ F) by VECTSP_1:def_7
.= (M - S) * (1_ F) by RLVECT_1:def_11 ;
hence  (1_ F) * (M - S) = K - R ; ::_thesis: verum
end;

theorem Th6: :: PARSP_2:6
for F being Field holds
not for a, b, c being Element of (MPS F) holds a,b '||' a,c
proof
let F be Field; ::_thesis: not for a, b, c being Element of (MPS F) holds a,b '||' a,c
consider e, f, g being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A1: e = [(1_ F),(1_ F),(0. F)] and
A2: f = [(- (0. F)),(1_ F),(0. F)] and
A3: g = [(1_ F),(- (0. F)),(0. F)] ;
A4: ( f `1_3 = - (0. F) & f `2_3 = 1_ F ) by A2, MCART_1:def_5, MCART_1:def_6;
A5: ( g `1_3 = 1_ F & g `2_3 = - (0. F) ) by A3, MCART_1:def_5, MCART_1:def_6;
 the carrier of (MPS F) = [: the carrier of F, the carrier of F, the carrier of F:] by PARSP_1:10;
then consider a, b, c being Element of (MPS F) such that
A6: [a,b,a,c] = [e,f,e,g] ;
take  a ; ::_thesis: not for b, c being Element of (MPS F) holds a,b '||' a,c
take  b ; ::_thesis: not for c being Element of (MPS F) holds a,b '||' a,c
take  c ; ::_thesis: not a,b '||' a,c
 ( e `1_3 = 1_ F & e `2_3 = 1_ F ) by A1, MCART_1:def_5, MCART_1:def_6;
then A7: (((e `1_3) - (f `1_3)) * ((e `2_3) - (g `2_3))) - (((e `1_3) - (g `1_3)) * ((e `2_3) - (f `2_3))) = (((1. F) + (- (- (0. F)))) * ((1. F) - (- (0. F)))) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by A4, A5, RLVECT_1:def_11
.= (((1. F) + (- (- (0. F)))) * ((1. F) + (- (- (0. F))))) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by RLVECT_1:def_11
.= (((1. F) + (0. F)) * ((1. F) + (- (- (0. F))))) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by RLVECT_1:17
.= (((1. F) + (0. F)) * ((1. F) + (0. F))) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by RLVECT_1:17
.= ((1. F) * ((1. F) + (0. F))) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by RLVECT_1:4
.= ((1. F) * (1. F)) - (((1. F) - (1. F)) * ((1. F) - (1. F))) by RLVECT_1:4
.= ((1. F) * (1. F)) - ((0. F) * ((1. F) - (1. F))) by RLVECT_1:15
.= ((1. F) * (1. F)) - (0. F) by VECTSP_1:12
.= (1. F) - (0. F) by VECTSP_1:def_8 ;
now__::_thesis:_for_e9,_f9,_g9,_h9_being_Element_of_[:_the_carrier_of_F,_the_carrier_of_F,_the_carrier_of_F:]_holds_
(_not_[e9,f9,g9,h9]_=_[a,b,a,c]_or_(((e9_`1_3)_-_(f9_`1_3))_*_((g9_`2_3)_-_(h9_`2_3)))_-_(((g9_`1_3)_-_(h9_`1_3))_*_((e9_`2_3)_-_(f9_`2_3)))_<>_0._F_or_(((e9_`1_3)_-_(f9_`1_3))_*_((g9_`3_3)_-_(h9_`3_3)))_-_(((g9_`1_3)_-_(h9_`1_3))_*_((e9_`3_3)_-_(f9_`3_3)))_<>_0._F_or_(((e9_`2_3)_-_(f9_`2_3))_*_((g9_`3_3)_-_(h9_`3_3)))_-_(((g9_`2_3)_-_(h9_`2_3))_*_((e9_`3_3)_-_(f9_`3_3)))_<>_0._F_)
let e9, f9, g9, h9 be Element of [: the carrier of F, the carrier of F, the carrier of F:]; ::_thesis: ( not [e9,f9,g9,h9] = [a,b,a,c] or (((e9 `1_3) - (f9 `1_3)) * ((g9 `2_3) - (h9 `2_3))) - (((g9 `1_3) - (h9 `1_3)) * ((e9 `2_3) - (f9 `2_3))) <> 0. F or (((e9 `1_3) - (f9 `1_3)) * ((g9 `3_3) - (h9 `3_3))) - (((g9 `1_3) - (h9 `1_3)) * ((e9 `3_3) - (f9 `3_3))) <> 0. F or (((e9 `2_3) - (f9 `2_3)) * ((g9 `3_3) - (h9 `3_3))) - (((g9 `2_3) - (h9 `2_3)) * ((e9 `3_3) - (f9 `3_3))) <> 0. F )
assume A8: [e9,f9,g9,h9] = [a,b,a,c] ; ::_thesis: ( (((e9 `1_3) - (f9 `1_3)) * ((g9 `2_3) - (h9 `2_3))) - (((g9 `1_3) - (h9 `1_3)) * ((e9 `2_3) - (f9 `2_3))) <> 0. F or (((e9 `1_3) - (f9 `1_3)) * ((g9 `3_3) - (h9 `3_3))) - (((g9 `1_3) - (h9 `1_3)) * ((e9 `3_3) - (f9 `3_3))) <> 0. F or (((e9 `2_3) - (f9 `2_3)) * ((g9 `3_3) - (h9 `3_3))) - (((g9 `2_3) - (h9 `2_3)) * ((e9 `3_3) - (f9 `3_3))) <> 0. F )
then A9: ( g9 = e & h9 = g ) by A6, XTUPLE_0:5;
 ( e9 = e & f9 = f ) by A6, A8, XTUPLE_0:5;
hence  ( (((e9 `1_3) - (f9 `1_3)) * ((g9 `2_3) - (h9 `2_3))) - (((g9 `1_3) - (h9 `1_3)) * ((e9 `2_3) - (f9 `2_3))) <> 0. F or (((e9 `1_3) - (f9 `1_3)) * ((g9 `3_3) - (h9 `3_3))) - (((g9 `1_3) - (h9 `1_3)) * ((e9 `3_3) - (f9 `3_3))) <> 0. F or (((e9 `2_3) - (f9 `2_3)) * ((g9 `3_3) - (h9 `3_3))) - (((g9 `2_3) - (h9 `2_3)) * ((e9 `3_3) - (f9 `3_3))) <> 0. F ) by A7, A9, Lm2; ::_thesis: verum
end;
hence  not a,b '||' a,c by PARSP_1:12; ::_thesis: verum
end;

theorem Th7: :: PARSP_2:7
for F being Field
for b, c, a, d being Element of (MPS F) st (1_ F) + (1_ F) <> 0. F & b,c '||' a,d & a,b '||' c,d & a,c '||' b,d holds
a,b '||' a,c
proof
let F be Field; ::_thesis: for b, c, a, d being Element of (MPS F) st (1_ F) + (1_ F) <> 0. F & b,c '||' a,d & a,b '||' c,d & a,c '||' b,d holds
a,b '||' a,c
let b, c, a, d be Element of (MPS F); ::_thesis: ( (1_ F) + (1_ F) <> 0. F & b,c '||' a,d & a,b '||' c,d & a,c '||' b,d implies a,b '||' a,c )
assume that
A1: (1_ F) + (1_ F) <> 0. F and
A2: b,c '||' a,d and
A3: a,b '||' c,d and
A4: a,c '||' b,d ; ::_thesis: a,b '||' a,c
assume A5: not a,b '||' a,c ; ::_thesis: contradiction
consider i, j, k, l being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A6: [b,c,a,d] = [i,j,k,l] and
A7: ( ex L being Element of F st
( L * ((i `1_3) - (j `1_3)) = (k `1_3) - (l `1_3) & L * ((i `2_3) - (j `2_3)) = (k `2_3) - (l `2_3) & L * ((i `3_3) - (j `3_3)) = (k `3_3) - (l `3_3) ) or ( (i `1_3) - (j `1_3) = 0. F & (i `2_3) - (j `2_3) = 0. F & (i `3_3) - (j `3_3) = 0. F ) ) by A2, Th2;
A8: ( b = i & c = j ) by A6, XTUPLE_0:5;
A9: ( a = k & d = l ) by A6, XTUPLE_0:5;
consider e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A10: [a,b,c,d] = [e,f,g,h] and
 ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) by A3, Th2;
A11: b = f by A10, XTUPLE_0:5;
A12: d = h by A10, XTUPLE_0:5;
A13: c = g by A10, XTUPLE_0:5;
A14: a = e by A10, XTUPLE_0:5;
then A15: [a,b,a,c] = [e,f,e,g] by A10, A11, XTUPLE_0:5;
 ( f = [(f `1_3),(f `2_3),(f `3_3)] & g = [(g `1_3),(g `2_3),(g `3_3)] ) by MCART_1:44;
then  ( i `1_3 <> j `1_3 or i `2_3 <> j `2_3 or i `3_3 <> j `3_3 ) by A5, A11, A13, A15, A8, Th3;
then consider L being Element of F such that
A16: L * ((f `1_3) - (g `1_3)) = (e `1_3) - (h `1_3) and
A17: L * ((f `2_3) - (g `2_3)) = (e `2_3) - (h `2_3) and
A18: L * ((f `3_3) - (g `3_3)) = (e `3_3) - (h `3_3) by A14, A11, A13, A12, A7, A8, A9, Lm2;
 h `2_3 = ((f `2_3) + (g `2_3)) - (e `2_3) by A3, A4, A5, A10, Th5;
then A19: (L - (1_ F)) * ((e `2_3) - (g `2_3)) = (L + (1_ F)) * ((e `2_3) - (f `2_3)) by A17, Lm9;
 h `3_3 = ((f `3_3) + (g `3_3)) - (e `3_3) by A3, A4, A5, A10, Th5;
then A20: (L - (1_ F)) * ((e `3_3) - (g `3_3)) = (L + (1_ F)) * ((e `3_3) - (f `3_3)) by A18, Lm9;
 h `1_3 = ((f `1_3) + (g `1_3)) - (e `1_3) by A3, A4, A5, A10, Th5;
then  (L - (1_ F)) * ((e `1_3) - (g `1_3)) = (L + (1_ F)) * ((e `1_3) - (f `1_3)) by A16, Lm9;
then  ( L + (1_ F) = 0. F & L - (1_ F) = 0. F ) by A5, A15, A19, A20, Th4;
then  (L + (1_ F)) - (L - (1_ F)) = (0. F) + (- (0. F)) by RLVECT_1:def_11;
then  (L + (1_ F)) - (L - (1_ F)) = 0. F by RLVECT_1:5;
then  (L + (1_ F)) + (- (L - (1_ F))) = 0. F by RLVECT_1:def_11;
then  (L + (1_ F)) + ((1_ F) + (- L)) = 0. F by RLVECT_1:33;
then  ((L + (1_ F)) + (1_ F)) + (- L) = 0. F by RLVECT_1:def_3;
then  (((1_ F) + (1_ F)) + L) + (- L) = 0. F by RLVECT_1:def_3;
then  ((1_ F) + (1_ F)) + (L + (- L)) = 0. F by RLVECT_1:def_3;
then  ((1_ F) + (1_ F)) + (0. F) = 0. F by RLVECT_1:5;
hence  contradiction by A1, RLVECT_1:4; ::_thesis: verum
end;

theorem Th8: :: PARSP_2:8
for F being Field
for a, p, b, c, q, r being Element of (MPS F) st not a,p '||' a,b & not a,p '||' a,c & a,p '||' b,q & a,p '||' c,r & a,b '||' p,q & a,c '||' p,r holds
b,c '||' q,r
proof
let F be Field; ::_thesis: for a, p, b, c, q, r being Element of (MPS F) st not a,p '||' a,b & not a,p '||' a,c & a,p '||' b,q & a,p '||' c,r & a,b '||' p,q & a,c '||' p,r holds
b,c '||' q,r
let a, p, b, c, q, r be Element of (MPS F); ::_thesis: ( not a,p '||' a,b & not a,p '||' a,c & a,p '||' b,q & a,p '||' c,r & a,b '||' p,q & a,c '||' p,r implies b,c '||' q,r )
assume that
A1: not a,p '||' a,b and
A2: not a,p '||' a,c and
A3: a,p '||' b,q and
A4: a,p '||' c,r and
A5: a,b '||' p,q and
A6: a,c '||' p,r ; ::_thesis: b,c '||' q,r
consider i, j, k, l being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A7: [a,p,c,r] = [i,j,k,l] and
 ( ex L being Element of F st
( L * ((i `1_3) - (j `1_3)) = (k `1_3) - (l `1_3) & L * ((i `2_3) - (j `2_3)) = (k `2_3) - (l `2_3) & L * ((i `3_3) - (j `3_3)) = (k `3_3) - (l `3_3) ) or ( (i `1_3) - (j `1_3) = 0. F & (i `2_3) - (j `2_3) = 0. F & (i `3_3) - (j `3_3) = 0. F ) ) by A4, Th2;
consider e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A8: [a,b,p,q] = [e,f,g,h] and
 ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) by A5, Th2;
A9: ( a = e & p = g ) by A8, XTUPLE_0:5;
A10: c = k by A7, XTUPLE_0:5;
then A11: [a,p,c,r] = [e,g,k,l] by A9, A7, XTUPLE_0:5;
then A12: l `1_3 = ((g `1_3) + (k `1_3)) - (e `1_3) by A2, A4, A6, Th5;
A13: b = f by A8, XTUPLE_0:5;
then A14: [a,p,b,q] = [e,g,f,h] by A8, A9, XTUPLE_0:5;
then  h `1_3 = ((g `1_3) + (f `1_3)) - (e `1_3) by A1, A3, A5, Th5;
then A15: (1_ F) * ((f `1_3) - (k `1_3)) = (h `1_3) - (l `1_3) by A12, Lm10;
A16: l `3_3 = ((g `3_3) + (k `3_3)) - (e `3_3) by A2, A4, A6, A11, Th5;
A17: l `2_3 = ((g `2_3) + (k `2_3)) - (e `2_3) by A2, A4, A6, A11, Th5;
 h `3_3 = ((g `3_3) + (f `3_3)) - (e `3_3) by A1, A3, A5, A14, Th5;
then A18: (1_ F) * ((f `3_3) - (k `3_3)) = (h `3_3) - (l `3_3) by A16, Lm10;
 h `2_3 = ((g `2_3) + (f `2_3)) - (e `2_3) by A1, A3, A5, A14, Th5;
then A19: (1_ F) * ((f `2_3) - (k `2_3)) = (h `2_3) - (l `2_3) by A17, Lm10;
 q = h by A8, XTUPLE_0:5;
then  [b,c,q,r] = [f,k,h,l] by A13, A7, A10, XTUPLE_0:5;
hence  b,c '||' q,r by A15, A19, A18, Th2; ::_thesis: verum
end;

definition
let IT be ParSp;
attrIT is FanodesSp-like  means :Def1: :: PARSP_2:def 1
( not for a, b, c being Element of IT holds a,b '||' a,c & ( for a, b, c, d being Element of IT st b,c '||' a,d & a,b '||' c,d & a,c '||' b,d holds
a,b '||' a,c ) & ( for a, b, c, p, q, r being Element of IT st not a,p '||' a,b & not a,p '||' a,c & a,p '||' b,q & a,p '||' c,r & a,b '||' p,q & a,c '||' p,r holds
b,c '||' q,r ) );
end;

:: deftheorem Def1 defines FanodesSp-like PARSP_2:def_1_:_
 for IT being ParSp holds
( IT is FanodesSp-like iff ( not for a, b, c being Element of IT holds a,b '||' a,c & ( for a, b, c, d being Element of IT st b,c '||' a,d & a,b '||' c,d & a,c '||' b,d holds
a,b '||' a,c ) & ( for a, b, c, p, q, r being Element of IT st not a,p '||' a,b & not a,p '||' a,c & a,p '||' b,q & a,p '||' c,r & a,b '||' p,q & a,c '||' p,r holds
b,c '||' q,r ) ) );

registration
cluster non empty strict ParSp-like FanodesSp-like for ParStr ;
existence
 ex b1 being ParSp st
( b1 is strict & b1 is FanodesSp-like )
proof
set FF = the Fanoian Field;
reconsider FdSp = MPS the Fanoian Field as ParSp by Th1;
 (1_ the Fanoian Field) + (1_ the Fanoian Field) <> 0. the Fanoian Field by VECTSP_1:def_19;
then A1: for a, b, c, d being Element of FdSp st b,c '||' a,d & a,b '||' c,d & a,c '||' b,d holds
a,b '||' a,c by Th7;
 ( not for a, b, c being Element of FdSp holds a,b '||' a,c & ( for a, b, c, p, q, r being Element of FdSp st not a,p '||' a,b & not a,p '||' a,c & a,p '||' b,q & a,p '||' c,r & a,b '||' p,q & a,c '||' p,r holds
b,c '||' q,r ) ) by Th6, Th8;
then  FdSp is FanodesSp-like by A1, Def1;
hence  ex b1 being ParSp st
( b1 is strict & b1 is FanodesSp-like ) ; ::_thesis: verum
end;
end;

definition
mode FanodesSp is FanodesSp-like ParSp;
end;


theorem Th9: :: PARSP_2:9
for FdSp being FanodesSp
for p, q being Element of FdSp st p <> q holds
ex r being Element of FdSp st not p,q '||' p,r
proof
let FdSp be FanodesSp; ::_thesis: for p, q being Element of FdSp st p <> q holds
ex r being Element of FdSp st not p,q '||' p,r
let p, q be Element of FdSp; ::_thesis: ( p <> q implies ex r being Element of FdSp st not p,q '||' p,r )
consider a, b, c being Element of FdSp such that
A1: not a,b '||' a,c by Def1;
assume  p <> q ; ::_thesis: not for r being Element of FdSp holds p,q '||' p,r
then  ( not p,q '||' p,a or not p,q '||' p,b or not p,q '||' p,c ) by A1, PARSP_1:38;
hence  not for r being Element of FdSp holds p,q '||' p,r ; ::_thesis: verum
end;

definition
let FdSp be FanodesSp;
let a, b, c be Element of FdSp;
preda,b,c is_collinear  means :Def2: :: PARSP_2:def 2
a,b '||' a,c;
end;

:: deftheorem Def2 defines is_collinear PARSP_2:def_2_:_
 for FdSp being FanodesSp
for a, b, c being Element of FdSp holds
( a,b,c is_collinear iff a,b '||' a,c );

theorem Th10: :: PARSP_2:10
for FdSp being FanodesSp
for a, b, c being Element of FdSp st a,b,c is_collinear holds
( a,c,b is_collinear & c,b,a is_collinear & b,a,c is_collinear & b,c,a is_collinear & c,a,b is_collinear )
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c being Element of FdSp st a,b,c is_collinear holds
( a,c,b is_collinear & c,b,a is_collinear & b,a,c is_collinear & b,c,a is_collinear & c,a,b is_collinear )
let a, b, c be Element of FdSp; ::_thesis: ( a,b,c is_collinear implies ( a,c,b is_collinear & c,b,a is_collinear & b,a,c is_collinear & b,c,a is_collinear & c,a,b is_collinear ) )
assume  a,b,c is_collinear ; ::_thesis: ( a,c,b is_collinear & c,b,a is_collinear & b,a,c is_collinear & b,c,a is_collinear & c,a,b is_collinear )
then A1: a,b '||' a,c by Def2;
then A2: ( b,a '||' b,c & b,c '||' b,a ) by PARSP_1:24;
A3: c,a '||' c,b by A1, PARSP_1:24;
 ( a,c '||' a,b & c,b '||' c,a ) by A1, PARSP_1:24;
hence  ( a,c,b is_collinear & c,b,a is_collinear & b,a,c is_collinear & b,c,a is_collinear & c,a,b is_collinear ) by A2, A3, Def2; ::_thesis: verum
end;

theorem Th11: :: PARSP_2:11
for FdSp being FanodesSp
for a, b, c, p, q, r being Element of FdSp st not a,b,c is_collinear & a,b '||' p,q & a,c '||' p,r & p <> q & p <> r holds
not p,q,r is_collinear
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, p, q, r being Element of FdSp st not a,b,c is_collinear & a,b '||' p,q & a,c '||' p,r & p <> q & p <> r holds
not p,q,r is_collinear
let a, b, c, p, q, r be Element of FdSp; ::_thesis: ( not a,b,c is_collinear & a,b '||' p,q & a,c '||' p,r & p <> q & p <> r implies not p,q,r is_collinear )
assume that
A1: not a,b,c is_collinear and
A2: ( a,b '||' p,q & a,c '||' p,r & p <> q & p <> r ) ; ::_thesis: not p,q,r is_collinear
 not a,b '||' a,c by A1, Def2;
then  not p,q '||' p,r by A2, PARSP_1:30;
hence  not p,q,r is_collinear by Def2; ::_thesis: verum
end;

theorem Th12: :: PARSP_2:12
for FdSp being FanodesSp
for a, b, c being Element of FdSp st ( a = b or b = c or c = a ) holds
a,b,c is_collinear
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c being Element of FdSp st ( a = b or b = c or c = a ) holds
a,b,c is_collinear
let a, b, c be Element of FdSp; ::_thesis: ( ( a = b or b = c or c = a ) implies a,b,c is_collinear )
assume  ( a = b or b = c or c = a ) ; ::_thesis: a,b,c is_collinear
then  a,b '||' a,c by PARSP_1:25;
hence  a,b,c is_collinear by Def2; ::_thesis: verum
end;

theorem Th13: :: PARSP_2:13
for FdSp being FanodesSp
for a, b, p, q, r being Element of FdSp st a <> b & a,b,p is_collinear & a,b,q is_collinear & a,b,r is_collinear holds
p,q,r is_collinear
proof
let FdSp be FanodesSp; ::_thesis: for a, b, p, q, r being Element of FdSp st a <> b & a,b,p is_collinear & a,b,q is_collinear & a,b,r is_collinear holds
p,q,r is_collinear
let a, b, p, q, r be Element of FdSp; ::_thesis: ( a <> b & a,b,p is_collinear & a,b,q is_collinear & a,b,r is_collinear implies p,q,r is_collinear )
assume that
A1: a <> b and
A2: a,b,p is_collinear and
A3: a,b,q is_collinear and
A4: a,b,r is_collinear ; ::_thesis: p,q,r is_collinear
A5: a,b '||' a,p by A2, Def2;
 a,b '||' a,r by A4, Def2;
then A6: a,b '||' p,r by A5, PARSP_1:35;
 a,b '||' a,q by A3, Def2;
then  a,b '||' p,q by A5, PARSP_1:35;
then  p,q '||' p,r by A1, A6, PARSP_1:def_12;
hence  p,q,r is_collinear by Def2; ::_thesis: verum
end;

theorem Th14: :: PARSP_2:14
for FdSp being FanodesSp
for p, q being Element of FdSp st p <> q holds
ex r being Element of FdSp st not p,q,r is_collinear
proof
let FdSp be FanodesSp; ::_thesis: for p, q being Element of FdSp st p <> q holds
ex r being Element of FdSp st not p,q,r is_collinear
let p, q be Element of FdSp; ::_thesis: ( p <> q implies ex r being Element of FdSp st not p,q,r is_collinear )
assume  p <> q ; ::_thesis: not for r being Element of FdSp holds p,q,r is_collinear
then consider r being Element of FdSp such that
A1: not p,q '||' p,r by Th9;
 not p,q,r is_collinear by A1, Def2;
hence  not for r being Element of FdSp holds p,q,r is_collinear ; ::_thesis: verum
end;

theorem Th15: :: PARSP_2:15
for FdSp being FanodesSp
for a, b, c, d being Element of FdSp st a,b,c is_collinear & a,b,d is_collinear holds
a,b '||' c,d
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d being Element of FdSp st a,b,c is_collinear & a,b,d is_collinear holds
a,b '||' c,d
let a, b, c, d be Element of FdSp; ::_thesis: ( a,b,c is_collinear & a,b,d is_collinear implies a,b '||' c,d )
assume  ( a,b,c is_collinear & a,b,d is_collinear ) ; ::_thesis: a,b '||' c,d
then  ( a,b '||' a,c & a,b '||' a,d ) by Def2;
hence  a,b '||' c,d by PARSP_1:35; ::_thesis: verum
end;

theorem Th16: :: PARSP_2:16
for FdSp being FanodesSp
for a, b, c, d being Element of FdSp st not a,b,c is_collinear & a,b '||' c,d holds
not a,b,d is_collinear
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d being Element of FdSp st not a,b,c is_collinear & a,b '||' c,d holds
not a,b,d is_collinear
let a, b, c, d be Element of FdSp; ::_thesis: ( not a,b,c is_collinear & a,b '||' c,d implies not a,b,d is_collinear )
assume that
A1: not a,b,c is_collinear and
A2: a,b '||' c,d ; ::_thesis: not a,b,d is_collinear
A3: now__::_thesis:_(_c_<>_d_&_a_<>_d_implies_not_a,b,d_is_collinear_)
assume that
A4: c <> d and
A5: a <> d ; ::_thesis: not a,b,d is_collinear
 ( a,c '||' c,a & c <> a ) by A1, Th12, PARSP_1:25;
then  not c,d,a is_collinear by A1, A2, A4, Th11;
then A6: not d,c,a is_collinear by Th10;
A7: d,a '||' a,d by PARSP_1:25;
 ( a <> b & d,c '||' a,b ) by A1, A2, Th12, PARSP_1:23;
hence  not a,b,d is_collinear by A5, A6, A7, Th11; ::_thesis: verum
end;
now__::_thesis:_not_a_=_d
assume  a = d ; ::_thesis: contradiction
then  a,b '||' a,c by A2, PARSP_1:23;
hence  contradiction by A1, Def2; ::_thesis: verum
end;
hence  not a,b,d is_collinear by A1, A3; ::_thesis: verum
end;

theorem Th17: :: PARSP_2:17
for FdSp being FanodesSp
for a, b, c, d, x being Element of FdSp st not a,b,c is_collinear & a,b '||' c,d & c <> d & a,b,x is_collinear holds
not c,d,x is_collinear
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d, x being Element of FdSp st not a,b,c is_collinear & a,b '||' c,d & c <> d & a,b,x is_collinear holds
not c,d,x is_collinear
let a, b, c, d, x be Element of FdSp; ::_thesis: ( not a,b,c is_collinear & a,b '||' c,d & c <> d & a,b,x is_collinear implies not c,d,x is_collinear )
assume A1: ( not a,b,c is_collinear & a,b '||' c,d & c <> d ) ; ::_thesis: ( not a,b,x is_collinear or not c,d,x is_collinear )
now__::_thesis:_(_c,d,x_is_collinear_&_a,b,x_is_collinear_implies_not_c,d,x_is_collinear_)
assume  c,d,x is_collinear ; ::_thesis: ( not a,b,x is_collinear or not c,d,x is_collinear )
then  c,d '||' c,x by Def2;
hence  ( not a,b,x is_collinear or not c,d,x is_collinear ) by A1, Th16, PARSP_1:26; ::_thesis: verum
end;
hence  ( not a,b,x is_collinear or not c,d,x is_collinear ) ; ::_thesis: verum
end;

theorem :: PARSP_2:18
for FdSp being FanodesSp
for o, a, b, x being Element of FdSp holds
( o,a,b is_collinear or not o,a,x is_collinear or not o,b,x is_collinear or o = x )
proof
let FdSp be FanodesSp; ::_thesis: for o, a, b, x being Element of FdSp holds
( o,a,b is_collinear or not o,a,x is_collinear or not o,b,x is_collinear or o = x )
let o, a, b, x be Element of FdSp; ::_thesis: ( o,a,b is_collinear or not o,a,x is_collinear or not o,b,x is_collinear or o = x )
assume A1: not o,a,b is_collinear ; ::_thesis: ( not o,a,x is_collinear or not o,b,x is_collinear or o = x )
now__::_thesis:_(_o,a,x_is_collinear_&_o,b,x_is_collinear_&_o,a,x_is_collinear_&_o,b,x_is_collinear_implies_o_=_x_)
assume that
A2: o,a,x is_collinear and
A3: o,b,x is_collinear ; ::_thesis: ( not o,a,x is_collinear or not o,b,x is_collinear or o = x )
 a,o,x is_collinear by A2, Th10;
then A4: a,o '||' a,x by Def2;
 b,o,x is_collinear by A3, Th10;
then A5: b,o '||' b,x by Def2;
 not a,b,o is_collinear by A1, Th10;
then  not a,b '||' a,o by Def2;
hence  ( not o,a,x is_collinear or not o,b,x is_collinear or o = x ) by A4, A5, PARSP_1:33; ::_thesis: verum
end;
hence  ( not o,a,x is_collinear or not o,b,x is_collinear or o = x ) ; ::_thesis: verum
end;

theorem :: PARSP_2:19
for FdSp being FanodesSp
for o, a, b, p, q being Element of FdSp st o <> a & o <> b & o,a,b is_collinear & o,a,p is_collinear & o,b,q is_collinear holds
a,b '||' p,q
proof
let FdSp be FanodesSp; ::_thesis: for o, a, b, p, q being Element of FdSp st o <> a & o <> b & o,a,b is_collinear & o,a,p is_collinear & o,b,q is_collinear holds
a,b '||' p,q
let o, a, b, p, q be Element of FdSp; ::_thesis: ( o <> a & o <> b & o,a,b is_collinear & o,a,p is_collinear & o,b,q is_collinear implies a,b '||' p,q )
assume that
A1: o <> a and
A2: o <> b and
A3: o,a,b is_collinear and
A4: o,a,p is_collinear and
A5: o,b,q is_collinear ; ::_thesis: a,b '||' p,q
A6: now__::_thesis:_(_o_<>_p_implies_a,b_'||'_p,q_)
A7: o,a '||' o,b by A3, Def2;
 o,a '||' o,p by A4, Def2;
then A8: o,b '||' o,p by A1, A7, PARSP_1:def_12;
 o,b '||' o,q by A5, Def2;
then  o,p '||' o,q by A2, A8, PARSP_1:def_12;
then A9: o,p '||' p,q by PARSP_1:24;
 o,b '||' a,b by A7, PARSP_1:24;
then A10: a,b '||' o,p by A2, A8, PARSP_1:def_12;
assume  o <> p ; ::_thesis: a,b '||' p,q
hence  a,b '||' p,q by A10, A9, PARSP_1:26; ::_thesis: verum
end;
now__::_thesis:_(_o_=_p_implies_a,b_'||'_p,q_)
assume A11: o = p ; ::_thesis: a,b '||' p,q
then  p,a '||' p,b by A3, Def2;
then A12: a,b '||' p,b by PARSP_1:24;
 p,b '||' p,q by A5, A11, Def2;
hence  a,b '||' p,q by A2, A11, A12, PARSP_1:26; ::_thesis: verum
end;
hence  a,b '||' p,q by A6; ::_thesis: verum
end;

theorem :: PARSP_2:20
for FdSp being FanodesSp
for a, b, c, d, p, q being Element of FdSp st not a,b '||' c,d & a,b,p is_collinear & a,b,q is_collinear & c,d,p is_collinear & c,d,q is_collinear holds
p = q
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d, p, q being Element of FdSp st not a,b '||' c,d & a,b,p is_collinear & a,b,q is_collinear & c,d,p is_collinear & c,d,q is_collinear holds
p = q
let a, b, c, d, p, q be Element of FdSp; ::_thesis: ( not a,b '||' c,d & a,b,p is_collinear & a,b,q is_collinear & c,d,p is_collinear & c,d,q is_collinear implies p = q )
assume that
A1: not a,b '||' c,d and
A2: ( a,b,p is_collinear & a,b,q is_collinear ) and
A3: ( c,d,p is_collinear & c,d,q is_collinear ) ; ::_thesis: p = q
 c,d '||' p,q by A3, Th15;
then A4: p,q '||' c,d by PARSP_1:23;
 a,b '||' p,q by A2, Th15;
then  p,q '||' a,b by PARSP_1:23;
hence  p = q by A1, A4, PARSP_1:def_12; ::_thesis: verum
end;

theorem :: PARSP_2:21
for FdSp being FanodesSp
for a, b, c, d being Element of FdSp st a <> b & a,b,c is_collinear & a,b '||' c,d holds
a,c '||' b,d
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d being Element of FdSp st a <> b & a,b,c is_collinear & a,b '||' c,d holds
a,c '||' b,d
let a, b, c, d be Element of FdSp; ::_thesis: ( a <> b & a,b,c is_collinear & a,b '||' c,d implies a,c '||' b,d )
assume that
A1: a <> b and
A2: a,b,c is_collinear and
A3: a,b '||' c,d ; ::_thesis: a,c '||' b,d
now__::_thesis:_(_b_<>_c_implies_a,c_'||'_b,d_)
A4: a,b '||' a,c by A2, Def2;
then  a,b '||' c,b by PARSP_1:24;
then  c,b '||' c,d by A1, A3, PARSP_1:def_12;
then A5: b,c '||' b,d by PARSP_1:24;
assume A6: b <> c ; ::_thesis: a,c '||' b,d
 b,c '||' a,c by A4, PARSP_1:24;
hence  a,c '||' b,d by A6, A5, PARSP_1:def_12; ::_thesis: verum
end;
hence  a,c '||' b,d by A3; ::_thesis: verum
end;

theorem :: PARSP_2:22
for FdSp being FanodesSp
for a, b, c, d being Element of FdSp st a <> b & a,b,c is_collinear & a,b '||' c,d holds
c,b '||' c,d
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d being Element of FdSp st a <> b & a,b,c is_collinear & a,b '||' c,d holds
c,b '||' c,d
let a, b, c, d be Element of FdSp; ::_thesis: ( a <> b & a,b,c is_collinear & a,b '||' c,d implies c,b '||' c,d )
assume that
A1: a <> b and
A2: a,b,c is_collinear and
A3: a,b '||' c,d ; ::_thesis: c,b '||' c,d
now__::_thesis:_(_a_<>_c_implies_c,b_'||'_c,d_)
 a,b '||' a,c by A2, Def2;
then A4: ( a,c '||' c,b & a,c '||' c,d ) by A1, A3, PARSP_1:24, PARSP_1:def_12;
assume  a <> c ; ::_thesis: c,b '||' c,d
hence  c,b '||' c,d by A4, PARSP_1:def_12; ::_thesis: verum
end;
hence  c,b '||' c,d by A3; ::_thesis: verum
end;

theorem :: PARSP_2:23
for FdSp being FanodesSp
for o, a, c, b, p, q being Element of FdSp st not o,a,c is_collinear & o,a,b is_collinear & o,c,p is_collinear & o,c,q is_collinear & a,c '||' b,p & a,c '||' b,q holds
p = q
proof
let FdSp be FanodesSp; ::_thesis: for o, a, c, b, p, q being Element of FdSp st not o,a,c is_collinear & o,a,b is_collinear & o,c,p is_collinear & o,c,q is_collinear & a,c '||' b,p & a,c '||' b,q holds
p = q
let o, a, c, b, p, q be Element of FdSp; ::_thesis: ( not o,a,c is_collinear & o,a,b is_collinear & o,c,p is_collinear & o,c,q is_collinear & a,c '||' b,p & a,c '||' b,q implies p = q )
assume that
A1: ( not o,a,c is_collinear & o,a,b is_collinear ) and
A2: ( o,c,p is_collinear & o,c,q is_collinear ) and
A3: ( a,c '||' b,p & a,c '||' b,q ) ; ::_thesis: p = q
A4: ( o,c '||' o,p & o,c '||' o,q ) by A2, Def2;
 ( not o,a '||' o,c & o,a '||' o,b ) by A1, Def2;
hence  p = q by A3, A4, PARSP_1:34; ::_thesis: verum
end;

theorem :: PARSP_2:24
for FdSp being FanodesSp
for a, b, c, d being Element of FdSp st a <> b & a,b,c is_collinear & a,b,d is_collinear holds
a,c,d is_collinear
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d being Element of FdSp st a <> b & a,b,c is_collinear & a,b,d is_collinear holds
a,c,d is_collinear
let a, b, c, d be Element of FdSp; ::_thesis: ( a <> b & a,b,c is_collinear & a,b,d is_collinear implies a,c,d is_collinear )
assume that
A1: a <> b and
A2: ( a,b,c is_collinear & a,b,d is_collinear ) ; ::_thesis: a,c,d is_collinear
 ( a,b '||' a,c & a,b '||' a,d ) by A2, Def2;
then  a,c '||' a,d by A1, PARSP_1:def_12;
hence  a,c,d is_collinear by Def2; ::_thesis: verum
end;

theorem :: PARSP_2:25
for FdSp being FanodesSp
for a, b, c, d being Element of FdSp st a,b,c is_collinear & a,c,d is_collinear & a <> c holds
b,c,d is_collinear
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d being Element of FdSp st a,b,c is_collinear & a,c,d is_collinear & a <> c holds
b,c,d is_collinear
let a, b, c, d be Element of FdSp; ::_thesis: ( a,b,c is_collinear & a,c,d is_collinear & a <> c implies b,c,d is_collinear )
assume that
A1: a,b,c is_collinear and
A2: ( a,c,d is_collinear & a <> c ) ; ::_thesis: b,c,d is_collinear
A3: a,c,c is_collinear by Th12;
 a,c,b is_collinear by A1, Th10;
hence  b,c,d is_collinear by A2, A3, Th13; ::_thesis: verum
end;

definition
let FdSp be FanodesSp;
let a, b, c, d be Element of FdSp;
pred parallelogram a,b,c,d means :Def3: :: PARSP_2:def 3
( not a,b,c is_collinear & a,b '||' c,d & a,c '||' b,d );
end;

:: deftheorem Def3 defines parallelogram PARSP_2:def_3_:_
 for FdSp being FanodesSp
for a, b, c, d being Element of FdSp holds
( parallelogram a,b,c,d iff ( not a,b,c is_collinear & a,b '||' c,d & a,c '||' b,d ) );

theorem Th26: :: PARSP_2:26
for FdSp being FanodesSp
for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
( a <> b & b <> c & c <> a & a <> d & b <> d & c <> d )
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
( a <> b & b <> c & c <> a & a <> d & b <> d & c <> d )
let a, b, c, d be Element of FdSp; ::_thesis: ( parallelogram a,b,c,d implies ( a <> b & b <> c & c <> a & a <> d & b <> d & c <> d ) )
assume A1: parallelogram a,b,c,d ; ::_thesis: ( a <> b & b <> c & c <> a & a <> d & b <> d & c <> d )
A2: now__::_thesis:_not_a_=_d
assume  a = d ; ::_thesis: contradiction
then  a,b '||' c,a by A1, Def3;
then A3: a,b '||' a,c by PARSP_1:23;
 not a,b,c is_collinear by A1, Def3;
hence  contradiction by A3, Def2; ::_thesis: verum
end;
A4: now__::_thesis:_not_c_=_d
assume  c = d ; ::_thesis: contradiction
then  a,c '||' b,c by A1, Def3;
then  c,a '||' c,b by PARSP_1:23;
then A5: a,b '||' a,c by PARSP_1:24;
 not a,b,c is_collinear by A1, Def3;
hence  contradiction by A5, Def2; ::_thesis: verum
end;
A6: now__::_thesis:_not_b_=_d
assume  b = d ; ::_thesis: contradiction
then  a,b '||' c,b by A1, Def3;
then  b,a '||' b,c by PARSP_1:23;
then A7: a,b '||' a,c by PARSP_1:24;
 not a,b,c is_collinear by A1, Def3;
hence  contradiction by A7, Def2; ::_thesis: verum
end;
 not a,b,c is_collinear by A1, Def3;
hence  ( a <> b & b <> c & c <> a & a <> d & b <> d & c <> d ) by A2, A6, A4, Th12; ::_thesis: verum
end;

theorem Th27: :: PARSP_2:27
for FdSp being FanodesSp
for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
( not a,b,c is_collinear & not b,a,d is_collinear & not c,d,a is_collinear & not d,c,b is_collinear )
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
( not a,b,c is_collinear & not b,a,d is_collinear & not c,d,a is_collinear & not d,c,b is_collinear )
let a, b, c, d be Element of FdSp; ::_thesis: ( parallelogram a,b,c,d implies ( not a,b,c is_collinear & not b,a,d is_collinear & not c,d,a is_collinear & not d,c,b is_collinear ) )
A1: ( a,b '||' b,a & a,c '||' c,a ) by PARSP_1:25;
assume A2: parallelogram a,b,c,d ; ::_thesis: ( not a,b,c is_collinear & not b,a,d is_collinear & not c,d,a is_collinear & not d,c,b is_collinear )
then A3: d <> b by Th26;
 a,c '||' b,d by A2, Def3;
then A4: a,c '||' d,b by PARSP_1:23;
 a,b '||' c,d by A2, Def3;
then A5: a,b '||' d,c by PARSP_1:23;
A6: ( not a,b,c is_collinear & d <> c ) by A2, Def3, Th26;
A7: ( a,b '||' c,d & c <> a ) by A2, Def3, Th26;
 ( a,c '||' b,d & b <> a ) by A2, Def3, Th26;
hence  ( not a,b,c is_collinear & not b,a,d is_collinear & not c,d,a is_collinear & not d,c,b is_collinear ) by A1, A7, A5, A4, A6, A3, Th11; ::_thesis: verum
end;

theorem Th28: :: PARSP_2:28
for FdSp being FanodesSp
for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
( not a,b,c is_collinear & not b,a,d is_collinear & not c,d,a is_collinear & not d,c,b is_collinear & not a,c,b is_collinear & not b,a,c is_collinear & not b,c,a is_collinear & not c,a,b is_collinear & not c,b,a is_collinear & not b,d,a is_collinear & not a,b,d is_collinear & not a,d,b is_collinear & not d,a,b is_collinear & not d,b,a is_collinear & not c,a,d is_collinear & not a,c,d is_collinear & not a,d,c is_collinear & not d,a,c is_collinear & not d,c,a is_collinear & not d,b,c is_collinear & not b,c,d is_collinear & not b,d,c is_collinear & not c,b,d is_collinear & not c,d,b is_collinear )
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
( not a,b,c is_collinear & not b,a,d is_collinear & not c,d,a is_collinear & not d,c,b is_collinear & not a,c,b is_collinear & not b,a,c is_collinear & not b,c,a is_collinear & not c,a,b is_collinear & not c,b,a is_collinear & not b,d,a is_collinear & not a,b,d is_collinear & not a,d,b is_collinear & not d,a,b is_collinear & not d,b,a is_collinear & not c,a,d is_collinear & not a,c,d is_collinear & not a,d,c is_collinear & not d,a,c is_collinear & not d,c,a is_collinear & not d,b,c is_collinear & not b,c,d is_collinear & not b,d,c is_collinear & not c,b,d is_collinear & not c,d,b is_collinear )
let a, b, c, d be Element of FdSp; ::_thesis: ( parallelogram a,b,c,d implies ( not a,b,c is_collinear & not b,a,d is_collinear & not c,d,a is_collinear & not d,c,b is_collinear & not a,c,b is_collinear & not b,a,c is_collinear & not b,c,a is_collinear & not c,a,b is_collinear & not c,b,a is_collinear & not b,d,a is_collinear & not a,b,d is_collinear & not a,d,b is_collinear & not d,a,b is_collinear & not d,b,a is_collinear & not c,a,d is_collinear & not a,c,d is_collinear & not a,d,c is_collinear & not d,a,c is_collinear & not d,c,a is_collinear & not d,b,c is_collinear & not b,c,d is_collinear & not b,d,c is_collinear & not c,b,d is_collinear & not c,d,b is_collinear ) )
assume A1: parallelogram a,b,c,d ; ::_thesis: ( not a,b,c is_collinear & not b,a,d is_collinear & not c,d,a is_collinear & not d,c,b is_collinear & not a,c,b is_collinear & not b,a,c is_collinear & not b,c,a is_collinear & not c,a,b is_collinear & not c,b,a is_collinear & not b,d,a is_collinear & not a,b,d is_collinear & not a,d,b is_collinear & not d,a,b is_collinear & not d,b,a is_collinear & not c,a,d is_collinear & not a,c,d is_collinear & not a,d,c is_collinear & not d,a,c is_collinear & not d,c,a is_collinear & not d,b,c is_collinear & not b,c,d is_collinear & not b,d,c is_collinear & not c,b,d is_collinear & not c,d,b is_collinear )
then A2: ( not c,d,a is_collinear & not d,c,b is_collinear ) by Th27;
 ( not a,b,c is_collinear & not b,a,d is_collinear ) by A1, Th27;
hence  ( not a,b,c is_collinear & not b,a,d is_collinear & not c,d,a is_collinear & not d,c,b is_collinear & not a,c,b is_collinear & not b,a,c is_collinear & not b,c,a is_collinear & not c,a,b is_collinear & not c,b,a is_collinear & not b,d,a is_collinear & not a,b,d is_collinear & not a,d,b is_collinear & not d,a,b is_collinear & not d,b,a is_collinear & not c,a,d is_collinear & not a,c,d is_collinear & not a,d,c is_collinear & not d,a,c is_collinear & not d,c,a is_collinear & not d,b,c is_collinear & not b,c,d is_collinear & not b,d,c is_collinear & not c,b,d is_collinear & not c,d,b is_collinear ) by A2, Th10; ::_thesis: verum
end;

theorem Th29: :: PARSP_2:29
for FdSp being FanodesSp
for a, b, c, d, x being Element of FdSp holds
( not parallelogram a,b,c,d or not a,b,x is_collinear or not c,d,x is_collinear )
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d, x being Element of FdSp holds
( not parallelogram a,b,c,d or not a,b,x is_collinear or not c,d,x is_collinear )
let a, b, c, d, x be Element of FdSp; ::_thesis: ( not parallelogram a,b,c,d or not a,b,x is_collinear or not c,d,x is_collinear )
assume A1: parallelogram a,b,c,d ; ::_thesis: ( not a,b,x is_collinear or not c,d,x is_collinear )
then A2: c <> d by Th26;
 ( not a,b,c is_collinear & a,b '||' c,d ) by A1, Def3;
hence  ( not a,b,x is_collinear or not c,d,x is_collinear ) by A2, Th17; ::_thesis: verum
end;

theorem Th30: :: PARSP_2:30
for FdSp being FanodesSp
for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
parallelogram a,c,b,d
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
parallelogram a,c,b,d
let a, b, c, d be Element of FdSp; ::_thesis: ( parallelogram a,b,c,d implies parallelogram a,c,b,d )
assume A1: parallelogram a,b,c,d ; ::_thesis: parallelogram a,c,b,d
then A2: a,c '||' b,d by Def3;
 ( not a,c,b is_collinear & a,b '||' c,d ) by A1, Def3, Th28;
hence  parallelogram a,c,b,d by A2, Def3; ::_thesis: verum
end;

theorem Th31: :: PARSP_2:31
for FdSp being FanodesSp
for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
parallelogram c,d,a,b
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
parallelogram c,d,a,b
let a, b, c, d be Element of FdSp; ::_thesis: ( parallelogram a,b,c,d implies parallelogram c,d,a,b )
assume A1: parallelogram a,b,c,d ; ::_thesis: parallelogram c,d,a,b
then  a,b '||' c,d by Def3;
then A2: c,d '||' a,b by PARSP_1:23;
 a,c '||' b,d by A1, Def3;
then A3: c,a '||' d,b by PARSP_1:23;
 not c,d,a is_collinear by A1, Th28;
hence  parallelogram c,d,a,b by A2, A3, Def3; ::_thesis: verum
end;

theorem Th32: :: PARSP_2:32
for FdSp being FanodesSp
for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
parallelogram b,a,d,c
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
parallelogram b,a,d,c
let a, b, c, d be Element of FdSp; ::_thesis: ( parallelogram a,b,c,d implies parallelogram b,a,d,c )
assume A1: parallelogram a,b,c,d ; ::_thesis: parallelogram b,a,d,c
then  a,b '||' c,d by Def3;
then A2: b,a '||' d,c by PARSP_1:23;
 a,c '||' b,d by A1, Def3;
then A3: b,d '||' a,c by PARSP_1:23;
 not b,a,d is_collinear by A1, Th28;
hence  parallelogram b,a,d,c by A2, A3, Def3; ::_thesis: verum
end;

theorem Th33: :: PARSP_2:33
for FdSp being FanodesSp
for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
( parallelogram a,c,b,d & parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram d,b,c,a & parallelogram b,d,a,c & parallelogram d,c,b,a )
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
( parallelogram a,c,b,d & parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram d,b,c,a & parallelogram b,d,a,c & parallelogram d,c,b,a )
let a, b, c, d be Element of FdSp; ::_thesis: ( parallelogram a,b,c,d implies ( parallelogram a,c,b,d & parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram d,b,c,a & parallelogram b,d,a,c & parallelogram d,c,b,a ) )
assume A1: parallelogram a,b,c,d ; ::_thesis: ( parallelogram a,c,b,d & parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram d,b,c,a & parallelogram b,d,a,c & parallelogram d,c,b,a )
then  parallelogram c,d,a,b by Th31;
then A2: parallelogram c,a,d,b by Th30;
 parallelogram b,a,d,c by A1, Th32;
hence  ( parallelogram a,c,b,d & parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram d,b,c,a & parallelogram b,d,a,c & parallelogram d,c,b,a ) by A1, A2, Th30, Th31; ::_thesis: verum
end;

theorem Th34: :: PARSP_2:34
for FdSp being FanodesSp
for a, b, c being Element of FdSp st not a,b,c is_collinear holds
ex d being Element of FdSp st parallelogram a,b,c,d
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c being Element of FdSp st not a,b,c is_collinear holds
ex d being Element of FdSp st parallelogram a,b,c,d
let a, b, c be Element of FdSp; ::_thesis: ( not a,b,c is_collinear implies ex d being Element of FdSp st parallelogram a,b,c,d )
consider d being Element of FdSp such that
A1: ( a,b '||' c,d & a,c '||' b,d ) by PARSP_1:def_12;
assume  not a,b,c is_collinear ; ::_thesis: ex d being Element of FdSp st parallelogram a,b,c,d
then  parallelogram a,b,c,d by A1, Def3;
hence  ex d being Element of FdSp st parallelogram a,b,c,d ; ::_thesis: verum
end;

theorem Th35: :: PARSP_2:35
for FdSp being FanodesSp
for a, b, c, p, q being Element of FdSp st parallelogram a,b,c,p & parallelogram a,b,c,q holds
p = q
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, p, q being Element of FdSp st parallelogram a,b,c,p & parallelogram a,b,c,q holds
p = q
let a, b, c, p, q be Element of FdSp; ::_thesis: ( parallelogram a,b,c,p & parallelogram a,b,c,q implies p = q )
assume that
A1: parallelogram a,b,c,p and
A2: parallelogram a,b,c,q ; ::_thesis: p = q
 a,b '||' c,p by A1, Def3;
then A3: ( b,c '||' c,b & b,a '||' c,p ) by PARSP_1:23, PARSP_1:25;
 a,b '||' c,q by A2, Def3;
then A4: b,a '||' c,q by PARSP_1:23;
 a,c '||' b,p by A1, Def3;
then A5: c,a '||' b,p by PARSP_1:23;
 a,c '||' b,q by A2, Def3;
then A6: c,a '||' b,q by PARSP_1:23;
 not b,c,a is_collinear by A1, Th28;
then  not b,c '||' b,a by Def2;
hence  p = q by A3, A4, A5, A6, PARSP_1:34; ::_thesis: verum
end;

theorem Th36: :: PARSP_2:36
for FdSp being FanodesSp
for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
not a,d '||' b,c
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
not a,d '||' b,c
let a, b, c, d be Element of FdSp; ::_thesis: ( parallelogram a,b,c,d implies not a,d '||' b,c )
assume A1: parallelogram a,b,c,d ; ::_thesis: not a,d '||' b,c
then  not a,b,c is_collinear by Def3;
then A2: not a,b '||' a,c by Def2;
 ( a,b '||' c,d & a,c '||' b,d ) by A1, Def3;
then  not b,c '||' a,d by A2, Def1;
hence  not a,d '||' b,c by PARSP_1:19; ::_thesis: verum
end;

theorem Th37: :: PARSP_2:37
for FdSp being FanodesSp
for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
not parallelogram a,b,d,c
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
not parallelogram a,b,d,c
let a, b, c, d be Element of FdSp; ::_thesis: ( parallelogram a,b,c,d implies not parallelogram a,b,d,c )
assume  parallelogram a,b,c,d ; ::_thesis: not parallelogram a,b,d,c
then  not a,d '||' b,c by Th36;
hence  not parallelogram a,b,d,c by Def3; ::_thesis: verum
end;

theorem Th38: :: PARSP_2:38
for FdSp being FanodesSp
for a, b being Element of FdSp st a <> b holds
ex c being Element of FdSp st
( a,b,c is_collinear & c <> a & c <> b )
proof
let FdSp be FanodesSp; ::_thesis: for a, b being Element of FdSp st a <> b holds
ex c being Element of FdSp st
( a,b,c is_collinear & c <> a & c <> b )
let a, b be Element of FdSp; ::_thesis: ( a <> b implies ex c being Element of FdSp st
( a,b,c is_collinear & c <> a & c <> b ) )
assume  a <> b ; ::_thesis: ex c being Element of FdSp st
( a,b,c is_collinear & c <> a & c <> b )
then consider p being Element of FdSp such that
A1: not a,b,p is_collinear by Th14;
consider q being Element of FdSp such that
A2: parallelogram a,b,p,q by A1, Th34;
 not p,q,b is_collinear by A2, Th28;
then consider c being Element of FdSp such that
A3: parallelogram p,q,b,c by Th34;
A4: p,q '||' b,c by A3, Def3;
 ( p <> q & a,b '||' p,q ) by A2, Def3, Th26;
then  a,b '||' b,c by A4, PARSP_1:26;
then  b,a '||' b,c by PARSP_1:23;
then  b,a,c is_collinear by Def2;
then A5: a,b,c is_collinear by Th10;
A6: not a,q '||' b,p by A2, Th36;
 p,b '||' q,c by A3, Def3;
then A7: a <> c by A6, PARSP_1:23;
 b <> c by A3, Th26;
hence  ex c being Element of FdSp st
( a,b,c is_collinear & c <> a & c <> b ) by A7, A5; ::_thesis: verum
end;

theorem Th39: :: PARSP_2:39
for FdSp being FanodesSp
for a, p, b, q, c, r being Element of FdSp st parallelogram a,p,b,q & parallelogram a,p,c,r holds
b,c '||' q,r
proof
let FdSp be FanodesSp; ::_thesis: for a, p, b, q, c, r being Element of FdSp st parallelogram a,p,b,q & parallelogram a,p,c,r holds
b,c '||' q,r
let a, p, b, q, c, r be Element of FdSp; ::_thesis: ( parallelogram a,p,b,q & parallelogram a,p,c,r implies b,c '||' q,r )
assume that
A1: parallelogram a,p,b,q and
A2: parallelogram a,p,c,r ; ::_thesis: b,c '||' q,r
A3: ( a,p '||' c,r & a,c '||' p,r ) by A2, Def3;
 not a,p,c is_collinear by A2, Def3;
then A4: not a,p '||' a,c by Def2;
 not a,p,b is_collinear by A1, Def3;
then A5: not a,p '||' a,b by Def2;
 ( a,p '||' b,q & a,b '||' p,q ) by A1, Def3;
hence  b,c '||' q,r by A5, A4, A3, Def1; ::_thesis: verum
end;

theorem Th40: :: PARSP_2:40
for FdSp being FanodesSp
for b, q, c, a, p, r being Element of FdSp st not b,q,c is_collinear & parallelogram a,p,b,q & parallelogram a,p,c,r holds
parallelogram b,q,c,r
proof
let FdSp be FanodesSp; ::_thesis: for b, q, c, a, p, r being Element of FdSp st not b,q,c is_collinear & parallelogram a,p,b,q & parallelogram a,p,c,r holds
parallelogram b,q,c,r
let b, q, c, a, p, r be Element of FdSp; ::_thesis: ( not b,q,c is_collinear & parallelogram a,p,b,q & parallelogram a,p,c,r implies parallelogram b,q,c,r )
assume that
A1: not b,q,c is_collinear and
A2: parallelogram a,p,b,q and
A3: parallelogram a,p,c,r ; ::_thesis: parallelogram b,q,c,r
A4: a,p '||' c,r by A3, Def3;
 ( a <> p & a,p '||' b,q ) by A2, Def3, Th26;
then A5: b,q '||' c,r by A4, PARSP_1:def_12;
 b,c '||' q,r by A2, A3, Th39;
hence  parallelogram b,q,c,r by A1, A5, Def3; ::_thesis: verum
end;

theorem Th41: :: PARSP_2:41
for FdSp being FanodesSp
for a, b, c, p, q, r being Element of FdSp st a,b,c is_collinear & b <> c & parallelogram a,p,b,q & parallelogram a,p,c,r holds
parallelogram b,q,c,r
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, p, q, r being Element of FdSp st a,b,c is_collinear & b <> c & parallelogram a,p,b,q & parallelogram a,p,c,r holds
parallelogram b,q,c,r
let a, b, c, p, q, r be Element of FdSp; ::_thesis: ( a,b,c is_collinear & b <> c & parallelogram a,p,b,q & parallelogram a,p,c,r implies parallelogram b,q,c,r )
assume that
A1: a,b,c is_collinear and
A2: b <> c and
A3: parallelogram a,p,b,q and
A4: parallelogram a,p,c,r ; ::_thesis: parallelogram b,q,c,r
A5: b <> q by A3, Th26;
 a,b '||' a,c by A1, Def2;
then A6: a,b '||' b,c by PARSP_1:24;
 ( not a,p,b is_collinear & a,p '||' b,q ) by A3, Def3;
hence  parallelogram b,q,c,r by A2, A3, A4, A5, A6, Th11, Th40; ::_thesis: verum
end;

theorem Th42: :: PARSP_2:42
for FdSp being FanodesSp
for a, p, b, q, c, r, d, s being Element of FdSp st parallelogram a,p,b,q & parallelogram a,p,c,r & parallelogram b,q,d,s holds
c,d '||' r,s
proof
let FdSp be FanodesSp; ::_thesis: for a, p, b, q, c, r, d, s being Element of FdSp st parallelogram a,p,b,q & parallelogram a,p,c,r & parallelogram b,q,d,s holds
c,d '||' r,s
let a, p, b, q, c, r, d, s be Element of FdSp; ::_thesis: ( parallelogram a,p,b,q & parallelogram a,p,c,r & parallelogram b,q,d,s implies c,d '||' r,s )
assume that
A1: parallelogram a,p,b,q and
A2: parallelogram a,p,c,r and
A3: parallelogram b,q,d,s ; ::_thesis: c,d '||' r,s
A4: now__::_thesis:_(_not_a,p,d_is_collinear_implies_c,d_'||'_r,s_)
assume A5: not a,p,d is_collinear ; ::_thesis: c,d '||' r,s
 parallelogram b,q,a,p by A1, Th33;
then  parallelogram a,p,d,s by A3, A5, Th40;
hence  c,d '||' r,s by A2, Th39; ::_thesis: verum
end;
A6: now__::_thesis:_(_b,q,c_is_collinear_&_a,p,d_is_collinear_implies_c,d_'||'_r,s_)
A7: a <> p by A1, Th26;
A8: ( not a,p,b is_collinear & a,p '||' a,p ) by A1, Th28, PARSP_1:25;
assume that
A9: b,q,c is_collinear and
A10: a,p,d is_collinear ; ::_thesis: c,d '||' r,s
 a <> b by A1, Th26;
then consider x being Element of FdSp such that
A11: a,b,x is_collinear and
A12: x <> a and
A13: x <> b by Th38;
 a,b '||' a,x by A11, Def2;
then consider y being Element of FdSp such that
A14: parallelogram a,p,x,y by A12, A8, A7, Th11, Th34;
A15: not x,y,d is_collinear by A10, A14, Th29;
 parallelogram b,q,x,y by A1, A11, A13, A14, Th41;
then A16: parallelogram x,y,d,s by A3, A15, Th40;
 not x,y,c is_collinear by A1, A9, A11, A13, A14, Th29, Th41;
then  parallelogram x,y,c,r by A2, A14, Th40;
hence  c,d '||' r,s by A16, Th39; ::_thesis: verum
end;
now__::_thesis:_(_not_b,q,c_is_collinear_implies_c,d_'||'_r,s_)
assume  not b,q,c is_collinear ; ::_thesis: c,d '||' r,s
then  parallelogram b,q,c,r by A1, A2, Th40;
hence  c,d '||' r,s by A3, Th39; ::_thesis: verum
end;
hence  c,d '||' r,s by A4, A6; ::_thesis: verum
end;

theorem Th43: :: PARSP_2:43
for FdSp being FanodesSp
for a, b being Element of FdSp st a <> b holds
ex c, d being Element of FdSp st parallelogram a,b,c,d
proof
let FdSp be FanodesSp; ::_thesis: for a, b being Element of FdSp st a <> b holds
ex c, d being Element of FdSp st parallelogram a,b,c,d
let a, b be Element of FdSp; ::_thesis: ( a <> b implies ex c, d being Element of FdSp st parallelogram a,b,c,d )
assume  a <> b ; ::_thesis: ex c, d being Element of FdSp st parallelogram a,b,c,d
then consider c being Element of FdSp such that
A1: not a,b,c is_collinear by Th14;
 ex d being Element of FdSp st parallelogram a,b,c,d by A1, Th34;
hence  ex c, d being Element of FdSp st parallelogram a,b,c,d ; ::_thesis: verum
end;

theorem :: PARSP_2:44
for FdSp being FanodesSp
for a, d being Element of FdSp st a <> d holds
ex b, c being Element of FdSp st parallelogram a,b,c,d
proof
let FdSp be FanodesSp; ::_thesis: for a, d being Element of FdSp st a <> d holds
ex b, c being Element of FdSp st parallelogram a,b,c,d
let a, d be Element of FdSp; ::_thesis: ( a <> d implies ex b, c being Element of FdSp st parallelogram a,b,c,d )
assume  a <> d ; ::_thesis: ex b, c being Element of FdSp st parallelogram a,b,c,d
then consider b being Element of FdSp such that
A1: not a,d,b is_collinear by Th14;
 not b,a,d is_collinear by A1, Th10;
then consider c being Element of FdSp such that
A2: parallelogram b,a,d,c by Th34;
 parallelogram a,b,c,d by A2, Th33;
hence  ex b, c being Element of FdSp st parallelogram a,b,c,d ; ::_thesis: verum
end;

definition
let FdSp be FanodesSp;
let a, b, r, s be Element of FdSp;
preda,b congr r,s means :Def4: :: PARSP_2:def 4
( ( a = b & r = s ) or ex p, q being Element of FdSp st
( parallelogram p,q,a,b & parallelogram p,q,r,s ) );
end;

:: deftheorem Def4 defines congr PARSP_2:def_4_:_
 for FdSp being FanodesSp
for a, b, r, s being Element of FdSp holds
( a,b congr r,s iff ( ( a = b & r = s ) or ex p, q being Element of FdSp st
( parallelogram p,q,a,b & parallelogram p,q,r,s ) ) );

theorem Th45: :: PARSP_2:45
for FdSp being FanodesSp
for a, b, c being Element of FdSp st a,a congr b,c holds
b = c
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c being Element of FdSp st a,a congr b,c holds
b = c
let a, b, c be Element of FdSp; ::_thesis: ( a,a congr b,c implies b = c )
assume  a,a congr b,c ; ::_thesis: b = c
then  ( ( a = a & b = c ) or ex p, q being Element of FdSp st
( parallelogram p,q,a,a & parallelogram p,q,b,c ) ) by Def4;
hence  b = c by Th26; ::_thesis: verum
end;

theorem :: PARSP_2:46
for FdSp being FanodesSp
for a, b, c being Element of FdSp st a,b congr c,c holds
a = b
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c being Element of FdSp st a,b congr c,c holds
a = b
let a, b, c be Element of FdSp; ::_thesis: ( a,b congr c,c implies a = b )
assume  a,b congr c,c ; ::_thesis: a = b
then  ( ( a = b & c = c ) or ex p, q being Element of FdSp st
( parallelogram p,q,a,b & parallelogram p,q,c,c ) ) by Def4;
hence  a = b by Th26; ::_thesis: verum
end;

theorem :: PARSP_2:47
for FdSp being FanodesSp
for a, b being Element of FdSp st a,b congr b,a holds
a = b
proof
let FdSp be FanodesSp; ::_thesis: for a, b being Element of FdSp st a,b congr b,a holds
a = b
let a, b be Element of FdSp; ::_thesis: ( a,b congr b,a implies a = b )
assume A1: a,b congr b,a ; ::_thesis: a = b
now__::_thesis:_not_a_<>_b
assume  a <> b ; ::_thesis: contradiction
then  ex p, q being Element of FdSp st
( parallelogram p,q,a,b & parallelogram p,q,b,a ) by A1, Def4;
hence  contradiction by Th37; ::_thesis: verum
end;
hence  a = b ; ::_thesis: verum
end;

theorem Th48: :: PARSP_2:48
for FdSp being FanodesSp
for a, b, c, d being Element of FdSp st a,b congr c,d holds
a,b '||' c,d
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d being Element of FdSp st a,b congr c,d holds
a,b '||' c,d
let a, b, c, d be Element of FdSp; ::_thesis: ( a,b congr c,d implies a,b '||' c,d )
assume A1: a,b congr c,d ; ::_thesis: a,b '||' c,d
now__::_thesis:_(_a_<>_b_implies_a,b_'||'_c,d_)
assume  a <> b ; ::_thesis: a,b '||' c,d
then consider p, q being Element of FdSp such that
A2: parallelogram p,q,a,b and
A3: parallelogram p,q,c,d by A1, Def4;
A4: p,q '||' c,d by A3, Def3;
 ( p <> q & p,q '||' a,b ) by A2, Def3, Th26;
hence  a,b '||' c,d by A4, PARSP_1:def_12; ::_thesis: verum
end;
hence  a,b '||' c,d by PARSP_1:20; ::_thesis: verum
end;

theorem Th49: :: PARSP_2:49
for FdSp being FanodesSp
for a, b, c, d being Element of FdSp st a,b congr c,d holds
a,c '||' b,d
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d being Element of FdSp st a,b congr c,d holds
a,c '||' b,d
let a, b, c, d be Element of FdSp; ::_thesis: ( a,b congr c,d implies a,c '||' b,d )
assume A1: a,b congr c,d ; ::_thesis: a,c '||' b,d
A2: now__::_thesis:_(_a_=_b_implies_a,c_'||'_b,d_)
assume A3: a = b ; ::_thesis: a,c '||' b,d
then  c = d by A1, Th45;
hence  a,c '||' b,d by A3, PARSP_1:25; ::_thesis: verum
end;
now__::_thesis:_(_a_<>_b_implies_a,c_'||'_b,d_)
assume  a <> b ; ::_thesis: a,c '||' b,d
then  ex p, q being Element of FdSp st
( parallelogram p,q,a,b & parallelogram p,q,c,d ) by A1, Def4;
hence  a,c '||' b,d by Th39; ::_thesis: verum
end;
hence  a,c '||' b,d by A2; ::_thesis: verum
end;

theorem Th50: :: PARSP_2:50
for FdSp being FanodesSp
for a, b, c, d being Element of FdSp st a,b congr c,d & not a,b,c is_collinear holds
parallelogram a,b,c,d
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d being Element of FdSp st a,b congr c,d & not a,b,c is_collinear holds
parallelogram a,b,c,d
let a, b, c, d be Element of FdSp; ::_thesis: ( a,b congr c,d & not a,b,c is_collinear implies parallelogram a,b,c,d )
assume that
A1: a,b congr c,d and
A2: not a,b,c is_collinear ; ::_thesis: parallelogram a,b,c,d
 ( a,b '||' c,d & a,c '||' b,d ) by A1, Th48, Th49;
hence  parallelogram a,b,c,d by A2, Def3; ::_thesis: verum
end;

theorem Th51: :: PARSP_2:51
for FdSp being FanodesSp
for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
a,b congr c,d
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds
a,b congr c,d
let a, b, c, d be Element of FdSp; ::_thesis: ( parallelogram a,b,c,d implies a,b congr c,d )
A1: a,b '||' a,b by PARSP_1:25;
assume A2: parallelogram a,b,c,d ; ::_thesis: a,b congr c,d
then A3: ( not a,c,b is_collinear & a <> b ) by Th26, Th28;
 a <> c by A2, Th26;
then consider p being Element of FdSp such that
A4: a,c,p is_collinear and
A5: a <> p and
A6: c <> p by Th38;
 a,c '||' a,p by A4, Def2;
then consider q being Element of FdSp such that
A7: parallelogram a,p,b,q by A5, A1, A3, Th11, Th34;
 parallelogram a,b,p,q by A7, Th33;
then  parallelogram c,d,p,q by A2, A4, A6, Th41;
then A8: parallelogram p,q,c,d by Th33;
 parallelogram p,q,a,b by A7, Th33;
hence  a,b congr c,d by A8, Def4; ::_thesis: verum
end;

theorem Th52: :: PARSP_2:52
for FdSp being FanodesSp
for a, b, c, d, r, s being Element of FdSp st a,b congr c,d & a,b,c is_collinear & parallelogram r,s,a,b holds
parallelogram r,s,c,d
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d, r, s being Element of FdSp st a,b congr c,d & a,b,c is_collinear & parallelogram r,s,a,b holds
parallelogram r,s,c,d
let a, b, c, d, r, s be Element of FdSp; ::_thesis: ( a,b congr c,d & a,b,c is_collinear & parallelogram r,s,a,b implies parallelogram r,s,c,d )
assume that
A1: a,b congr c,d and
A2: a,b,c is_collinear and
A3: parallelogram r,s,a,b ; ::_thesis: parallelogram r,s,c,d
now__::_thesis:_(_a_<>_b_implies_parallelogram_r,s,c,d_)
assume A4: a <> b ; ::_thesis: parallelogram r,s,c,d
then consider p, q being Element of FdSp such that
A5: parallelogram p,q,a,b and
A6: parallelogram p,q,c,d by A1, Def4;
 ( r,s '||' a,b & a,b '||' c,d ) by A1, A3, Def3, Th48;
then A7: r,s '||' c,d by A4, PARSP_1:26;
A8: parallelogram a,b,r,s by A3, Th33;
 parallelogram a,b,p,q by A5, Th33;
then A9: r,c '||' s,d by A6, A8, Th42;
 not r,s,c is_collinear by A2, A3, Th29;
hence  parallelogram r,s,c,d by A7, A9, Def3; ::_thesis: verum
end;
hence  parallelogram r,s,c,d by A3, Th26; ::_thesis: verum
end;

theorem :: PARSP_2:53
for FdSp being FanodesSp
for a, b, c, x, y being Element of FdSp st a,b congr c,x & a,b congr c,y holds
x = y
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, x, y being Element of FdSp st a,b congr c,x & a,b congr c,y holds
x = y
let a, b, c, x, y be Element of FdSp; ::_thesis: ( a,b congr c,x & a,b congr c,y implies x = y )
assume that
A1: a,b congr c,x and
A2: a,b congr c,y ; ::_thesis: x = y
A3: now__::_thesis:_(_a_<>_b_&_not_a,b,c_is_collinear_implies_x_=_y_)
assume that
 a <> b and
A4: not a,b,c is_collinear ; ::_thesis: x = y
 ( parallelogram a,b,c,x & parallelogram a,b,c,y ) by A1, A2, A4, Th50;
hence  x = y by Th35; ::_thesis: verum
end;
A5: now__::_thesis:_(_a_<>_b_&_a,b,c_is_collinear_implies_x_=_y_)
assume that
A6: a <> b and
A7: a,b,c is_collinear ; ::_thesis: x = y
consider p, q being Element of FdSp such that
A8: parallelogram a,b,p,q by A6, Th43;
 parallelogram p,q,a,b by A8, Th33;
then  ( parallelogram p,q,c,x & parallelogram p,q,c,y ) by A1, A2, A7, Th52;
hence  x = y by Th35; ::_thesis: verum
end;
now__::_thesis:_(_a_=_b_implies_x_=_y_)
assume A9: a = b ; ::_thesis: x = y
then  c = x by A1, Th45;
hence  x = y by A2, A9, Th45; ::_thesis: verum
end;
hence  x = y by A5, A3; ::_thesis: verum
end;

theorem :: PARSP_2:54
for FdSp being FanodesSp
for a, b, c being Element of FdSp ex d being Element of FdSp st a,b congr c,d
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c being Element of FdSp ex d being Element of FdSp st a,b congr c,d
let a, b, c be Element of FdSp; ::_thesis: ex d being Element of FdSp st a,b congr c,d
A1: now__::_thesis:_(_a_=_b_implies_ex_d_being_Element_of_FdSp_st_a,b_congr_c,d_)
assume  a = b ; ::_thesis: ex d being Element of FdSp st a,b congr c,d
then  a,b congr c,c by Def4;
hence  ex d being Element of FdSp st a,b congr c,d ; ::_thesis: verum
end;
A2: now__::_thesis:_(_a_<>_b_&_a,b,c_is_collinear_implies_ex_d_being_Element_of_FdSp_st_a,b_congr_c,d_)
assume that
A3: a <> b and
A4: a,b,c is_collinear ; ::_thesis: ex d being Element of FdSp st a,b congr c,d
consider p, q being Element of FdSp such that
A5: parallelogram a,b,p,q by A3, Th43;
 not p,q,c is_collinear by A4, A5, Th29;
then consider d being Element of FdSp such that
A6: parallelogram p,q,c,d by Th34;
 parallelogram p,q,a,b by A5, Th33;
then  a,b congr c,d by A6, Def4;
hence  ex d being Element of FdSp st a,b congr c,d ; ::_thesis: verum
end;
now__::_thesis:_(_a_<>_b_&_not_a,b,c_is_collinear_implies_ex_d_being_Element_of_FdSp_st_a,b_congr_c,d_)
assume that
 a <> b and
A7: not a,b,c is_collinear ; ::_thesis: ex d being Element of FdSp st a,b congr c,d
 ex d being Element of FdSp st parallelogram a,b,c,d by A7, Th34;
hence  ex d being Element of FdSp st a,b congr c,d by Th51; ::_thesis: verum
end;
hence  ex d being Element of FdSp st a,b congr c,d by A1, A2; ::_thesis: verum
end;

theorem Th55: :: PARSP_2:55
for FdSp being FanodesSp
for a, b being Element of FdSp holds a,b congr a,b
proof
let FdSp be FanodesSp; ::_thesis: for a, b being Element of FdSp holds a,b congr a,b
let a, b be Element of FdSp; ::_thesis: a,b congr a,b
now__::_thesis:_(_a_<>_b_implies_a,b_congr_a,b_)
assume  a <> b ; ::_thesis: a,b congr a,b
then consider p, q being Element of FdSp such that
A1: parallelogram a,b,p,q by Th43;
 parallelogram p,q,a,b by A1, Th33;
hence  a,b congr a,b by Def4; ::_thesis: verum
end;
hence  a,b congr a,b by Def4; ::_thesis: verum
end;

theorem Th56: :: PARSP_2:56
for FdSp being FanodesSp
for r, s, a, b, c, d being Element of FdSp st r,s congr a,b & r,s congr c,d holds
a,b congr c,d
proof
let FdSp be FanodesSp; ::_thesis: for r, s, a, b, c, d being Element of FdSp st r,s congr a,b & r,s congr c,d holds
a,b congr c,d
let r, s, a, b, c, d be Element of FdSp; ::_thesis: ( r,s congr a,b & r,s congr c,d implies a,b congr c,d )
assume that
A1: r,s congr a,b and
A2: r,s congr c,d ; ::_thesis: a,b congr c,d
A3: now__::_thesis:_(_r_<>_s_&_not_r,s,a_is_collinear_&_not_r,s,c_is_collinear_implies_a,b_congr_c,d_)
assume that
 r <> s and
A4: ( not r,s,a is_collinear & not r,s,c is_collinear ) ; ::_thesis: a,b congr c,d
 ( parallelogram r,s,a,b & parallelogram r,s,c,d ) by A1, A2, A4, Th50;
hence  a,b congr c,d by Def4; ::_thesis: verum
end;
A5: now__::_thesis:_(_r_<>_s_&_r,s,c_is_collinear_implies_a,b_congr_c,d_)
assume that
A6: r <> s and
A7: r,s,c is_collinear ; ::_thesis: a,b congr c,d
consider p, q being Element of FdSp such that
A8: parallelogram p,q,r,s and
A9: parallelogram p,q,a,b by A1, A6, Def4;
 parallelogram p,q,c,d by A2, A7, A8, Th52;
hence  a,b congr c,d by A9, Def4; ::_thesis: verum
end;
A10: now__::_thesis:_(_r_<>_s_&_r,s,a_is_collinear_implies_a,b_congr_c,d_)
assume that
A11: r <> s and
A12: r,s,a is_collinear ; ::_thesis: a,b congr c,d
consider p, q being Element of FdSp such that
A13: parallelogram p,q,r,s and
A14: parallelogram p,q,c,d by A2, A11, Def4;
 parallelogram p,q,a,b by A1, A12, A13, Th52;
hence  a,b congr c,d by A14, Def4; ::_thesis: verum
end;
now__::_thesis:_(_r_=_s_implies_a,b_congr_c,d_)
assume  r = s ; ::_thesis: a,b congr c,d
then  ( a = b & c = d ) by A1, A2, Th45;
hence  a,b congr c,d by Def4; ::_thesis: verum
end;
hence  a,b congr c,d by A10, A5, A3; ::_thesis: verum
end;

theorem :: PARSP_2:57
for FdSp being FanodesSp
for a, b, c, d being Element of FdSp st a,b congr c,d holds
c,d congr a,b
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d being Element of FdSp st a,b congr c,d holds
c,d congr a,b
let a, b, c, d be Element of FdSp; ::_thesis: ( a,b congr c,d implies c,d congr a,b )
assume A1: a,b congr c,d ; ::_thesis: c,d congr a,b
 a,b congr a,b by Th55;
hence  c,d congr a,b by A1, Th56; ::_thesis: verum
end;

theorem :: PARSP_2:58
for FdSp being FanodesSp
for a, b, c, d being Element of FdSp st a,b congr c,d holds
b,a congr d,c
proof
let FdSp be FanodesSp; ::_thesis: for a, b, c, d being Element of FdSp st a,b congr c,d holds
b,a congr d,c
let a, b, c, d be Element of FdSp; ::_thesis: ( a,b congr c,d implies b,a congr d,c )
assume A1: a,b congr c,d ; ::_thesis: b,a congr d,c
A2: now__::_thesis:_(_a_<>_b_implies_b,a_congr_d,c_)
assume  a <> b ; ::_thesis: b,a congr d,c
then consider p, q being Element of FdSp such that
A3: ( parallelogram p,q,a,b & parallelogram p,q,c,d ) by A1, Def4;
 ( parallelogram q,p,b,a & parallelogram q,p,d,c ) by A3, Th33;
hence  b,a congr d,c by Def4; ::_thesis: verum
end;
now__::_thesis:_(_a_=_b_implies_b,a_congr_d,c_)
assume A4: a = b ; ::_thesis: b,a congr d,c
then  c = d by A1, Th45;
hence  b,a congr d,c by A4, Def4; ::_thesis: verum
end;
hence  b,a congr d,c by A2; ::_thesis: verum
end;