:: PARSP_1 semantic presentation

Lemma1: for b1 being non empty add-associative right_zeroed right_complementable LoopStr
for b2, b3 being Element of b1 holds - (b2 - b3) = b3 - b2
proof end;

Lemma2: for b1 being Field
for b2, b3, b4, b5 being Element of b1 holds ((b2 - b3) * (b4 - b5)) - ((b3 - b2) * (b5 - b4)) = 0. b1
proof end;

Lemma3: for b1 being Field
for b2, b3, b4, b5 being Element of b1 holds (b2 * (b3 - b3)) - ((b4 - b4) * b5) = 0. b1
proof end;

Lemma4: for b1 being Field
for b2, b3, b4, b5, b6, b7 being Element of b1 st b2 <> 0. b1 & (b2 * b3) - (b4 * b5) = 0. b1 & (b2 * b6) - (b7 * b5) = 0. b1 holds
(b4 * b6) - (b7 * b3) = 0. b1
proof end;

Lemma5: for b1 being Field
for b2, b3, b4, b5 being Element of b1 st (b2 * b3) - (b4 * b5) = 0. b1 holds
(b5 * b4) - (b3 * b2) = 0. b1
proof end;

Lemma6: for b1 being Field
for b2, b3, b4, b5, b6, b7 being Element of b1 st b2 <> 0. b1 & (b3 * b4) - (b5 * b2) = 0. b1 & (b3 * b6) - (b7 * b2) = 0. b1 holds
(b5 * b6) - (b7 * b4) = 0. b1
proof end;

Lemma7: for b1 being Field
for b2, b3, b4, b5 being Element of b1 holds (b2 * b3) * (b4 * b5) = ((b4 * b2) * b3) * b5
proof end;

Lemma8: for b1 being Field
for b2, b3, b4, b5, b6, b7 being Element of b1 st (b2 * b3) - (b4 * b5) = 0. b1 holds
(((b2 * b6) * b7) * b3) - (((b4 * b6) * b7) * b5) = 0. b1
proof end;

Lemma9: for b1 being Field
for b2, b3, b4, b5 being Element of b1 holds (b2 - b3) * (b4 - b5) = (b2 * b4) + ((- (b2 * b5)) + (- (b3 * (b4 - b5))))
proof end;

Lemma10: for b1 being Field
for b2, b3, b4, b5 being Element of b1 holds (b2 + b3) + (b4 + b5) = (b2 + (b3 + b4)) + b5
proof end;

Lemma11: for b1 being non empty add-associative right_zeroed right_complementable LoopStr
for b2, b3, b4 being Element of b1 holds (b3 + b2) - (b4 + b2) = b3 - b4
proof end;

Lemma12: for b1 being non empty add-associative right_zeroed right_complementable LoopStr
for b2, b3 being Element of b1 holds b2 + b3 = - ((- b3) + (- b2))
proof end;

Lemma13: for b1 being Field
for b2, b3, b4, b5, b6, b7 being Element of b1 st ((b2 - b3) * (b4 - b5)) - ((b2 - b6) * (b4 - b7)) = 0. b1 holds
((b3 - b2) * (b7 - b5)) - ((b3 - b6) * (b7 - b4)) = 0. b1
proof end;

Lemma14: for b1 being Field
for b2, b3, b4 being Element of b1 holds b2 - ((b2 + b3) + (- b4)) = b4 - b3
proof end;

Lemma15: for b1 being Field
for b2, b3, b4, b5, b6, b7 being Element of b1 holds ((b2 - b3) * (b4 - ((b4 + b5) + (- b6)))) - ((b7 - ((b7 + b3) + (- b2))) * (b6 - b5)) = 0. b1
proof end;

deffunc H1( Field) -> set = [:the carrier of a1,the carrier of a1,the carrier of a1:];

definition
let c1 be Field;
func c3add c1 -> BinOp of [:the carrier of a1,the carrier of a1,the carrier of a1:] means :Def1: :: PARSP_1:def 1
for b1, b2 being Element of [:the carrier of a1,the carrier of a1,the carrier of a1:] holds a2 . b1,b2 = [((b1 `1 ) + (b2 `1 )),((b1 `2 ) + (b2 `2 )),((b1 `3 ) + (b2 `3 ))];
existence
ex b1 being BinOp of [:the carrier of c1,the carrier of c1,the carrier of c1:] st
for b2, b3 being Element of [:the carrier of c1,the carrier of c1,the carrier of c1:] holds b1 . b2,b3 = [((b2 `1 ) + (b3 `1 )),((b2 `2 ) + (b3 `2 )),((b2 `3 ) + (b3 `3 ))]
proof end;
uniqueness
for b1, b2 being BinOp of [:the carrier of c1,the carrier of c1,the carrier of c1:] st ( for b3, b4 being Element of [:the carrier of c1,the carrier of c1,the carrier of c1:] holds b1 . b3,b4 = [((b3 `1 ) + (b4 `1 )),((b3 `2 ) + (b4 `2 )),((b3 `3 ) + (b4 `3 ))] ) & ( for b3, b4 being Element of [:the carrier of c1,the carrier of c1,the carrier of c1:] holds b2 . b3,b4 = [((b3 `1 ) + (b4 `1 )),((b3 `2 ) + (b4 `2 )),((b3 `3 ) + (b4 `3 ))] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines c3add PARSP_1:def 1 :
for b1 being Field
for b2 being BinOp of [:the carrier of b1,the carrier of b1,the carrier of b1:] holds
( b2 = c3add b1 iff for b3, b4 being Element of [:the carrier of b1,the carrier of b1,the carrier of b1:] holds b2 . b3,b4 = [((b3 `1 ) + (b4 `1 )),((b3 `2 ) + (b4 `2 )),((b3 `3 ) + (b4 `3 ))] );

definition
let c1 be Field;
let c2, c3 be Element of [:the carrier of c1,the carrier of c1,the carrier of c1:];
func c2 + c3 -> Element of [:the carrier of a1,the carrier of a1,the carrier of a1:] equals :: PARSP_1:def 2
(c3add a1) . a2,a3;
coherence
(c3add c1) . c2,c3 is Element of [:the carrier of c1,the carrier of c1,the carrier of c1:] ;
end;

:: deftheorem Def2 defines + PARSP_1:def 2 :
for b1 being Field
for b2, b3 being Element of [:the carrier of b1,the carrier of b1,the carrier of b1:] holds b2 + b3 = (c3add b1) . b2,b3;

theorem Th1: :: PARSP_1:1
canceled;

theorem Th2: :: PARSP_1:2
canceled;

theorem Th3: :: PARSP_1:3
for b1 being Field
for b2, b3 being Element of [:the carrier of b1,the carrier of b1,the carrier of b1:] holds b2 + b3 = [((b2 `1 ) + (b3 `1 )),((b2 `2 ) + (b3 `2 )),((b2 `3 ) + (b3 `3 ))] by Def1;

theorem Th4: :: PARSP_1:4
for b1 being Field
for b2, b3, b4, b5, b6, b7 being Element of b1 holds [b2,b3,b4] + [b5,b6,b7] = [(b2 + b5),(b3 + b6),(b4 + b7)]
proof end;

definition
let c1 be Field;
func c3compl c1 -> UnOp of [:the carrier of a1,the carrier of a1,the carrier of a1:] means :Def3: :: PARSP_1:def 3
for b1 being Element of [:the carrier of a1,the carrier of a1,the carrier of a1:] holds a2 . b1 = [(- (b1 `1 )),(- (b1 `2 )),(- (b1 `3 ))];
existence
ex b1 being UnOp of [:the carrier of c1,the carrier of c1,the carrier of c1:] st
for b2 being Element of [:the carrier of c1,the carrier of c1,the carrier of c1:] holds b1 . b2 = [(- (b2 `1 )),(- (b2 `2 )),(- (b2 `3 ))]
proof end;
uniqueness
for b1, b2 being UnOp of [:the carrier of c1,the carrier of c1,the carrier of c1:] st ( for b3 being Element of [:the carrier of c1,the carrier of c1,the carrier of c1:] holds b1 . b3 = [(- (b3 `1 )),(- (b3 `2 )),(- (b3 `3 ))] ) & ( for b3 being Element of [:the carrier of c1,the carrier of c1,the carrier of c1:] holds b2 . b3 = [(- (b3 `1 )),(- (b3 `2 )),(- (b3 `3 ))] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines c3compl PARSP_1:def 3 :
for b1 being Field
for b2 being UnOp of [:the carrier of b1,the carrier of b1,the carrier of b1:] holds
( b2 = c3compl b1 iff for b3 being Element of [:the carrier of b1,the carrier of b1,the carrier of b1:] holds b2 . b3 = [(- (b3 `1 )),(- (b3 `2 )),(- (b3 `3 ))] );

definition
let c1 be Field;
let c2 be Element of [:the carrier of c1,the carrier of c1,the carrier of c1:];
func - c2 -> Element of [:the carrier of a1,the carrier of a1,the carrier of a1:] equals :: PARSP_1:def 4
(c3compl a1) . a2;
coherence
(c3compl c1) . c2 is Element of [:the carrier of c1,the carrier of c1,the carrier of c1:] ;
end;

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

theorem Th5: :: PARSP_1:5
canceled;

theorem Th6: :: PARSP_1:6
canceled;

theorem Th7: :: PARSP_1:7
for b1 being Field
for b2 being Element of [:the carrier of b1,the carrier of b1,the carrier of b1:] holds - b2 = [(- (b2 `1 )),(- (b2 `2 )),(- (b2 `3 ))] by Def3;

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

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

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

registration
cluster non empty ParStr ;
existence
not for b1 being ParStr holds b1 is empty
proof end;
end;

definition
let c1 be non empty ParStr ;
let c2, c3, c4, c5 be Element of c1;
pred c2,c3 '||' c4,c5 means :Def6: :: PARSP_1:def 6
[a2,a3,a4,a5] in the 4_arg_relation of a1;
end;

:: deftheorem Def6 defines '||' PARSP_1:def 6 :
for b1 being non empty ParStr
for b2, b3, b4, b5 being Element of b1 holds
( b2,b3 '||' b4,b5 iff [b2,b3,b4,b5] in the 4_arg_relation of b1 );

definition
let c1 be Field;
func C3 c1 -> set equals :: PARSP_1:def 7
[:the carrier of a1,the carrier of a1,the carrier of a1:];
coherence
[:the carrier of c1,the carrier of c1,the carrier of c1:] is set ;
end;

:: deftheorem Def7 defines C3 PARSP_1:def 7 :
for b1 being Field holds C3 b1 = [:the carrier of b1,the carrier of b1,the carrier of b1:];

registration
let c1 be Field;
cluster C3 a1 -> non empty ;
coherence
not C3 c1 is empty ;
end;

definition
let c1 be Field;
func 4C3 c1 -> set equals :: PARSP_1:def 8
[:(C3 a1),(C3 a1),(C3 a1),(C3 a1):];
coherence
[:(C3 c1),(C3 c1),(C3 c1),(C3 c1):] is set ;
end;

:: deftheorem Def8 defines 4C3 PARSP_1:def 8 :
for b1 being Field holds 4C3 b1 = [:(C3 b1),(C3 b1),(C3 b1),(C3 b1):];

registration
let c1 be Field;
cluster 4C3 a1 -> non empty ;
coherence
not 4C3 c1 is empty ;
end;

definition
let c1 be Field;
func PRs c1 -> set means :Def9: :: PARSP_1:def 9
for b1 being set holds
( b1 in a2 iff ( b1 in 4C3 a1 & ex b2, b3, b4, b5 being Element of [:the carrier of a1,the carrier of a1,the carrier of a1:] st
( b1 = [b2,b3,b4,b5] & (((b2 `1 ) - (b3 `1 )) * ((b4 `2 ) - (b5 `2 ))) - (((b4 `1 ) - (b5 `1 )) * ((b2 `2 ) - (b3 `2 ))) = 0. a1 & (((b2 `1 ) - (b3 `1 )) * ((b4 `3 ) - (b5 `3 ))) - (((b4 `1 ) - (b5 `1 )) * ((b2 `3 ) - (b3 `3 ))) = 0. a1 & (((b2 `2 ) - (b3 `2 )) * ((b4 `3 ) - (b5 `3 ))) - (((b4 `2 ) - (b5 `2 )) * ((b2 `3 ) - (b3 `3 ))) = 0. a1 ) ) );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff ( b2 in 4C3 c1 & ex b3, b4, b5, b6 being Element of [:the carrier of c1,the carrier of c1,the carrier of c1:] st
( b2 = [b3,b4,b5,b6] & (((b3 `1 ) - (b4 `1 )) * ((b5 `2 ) - (b6 `2 ))) - (((b5 `1 ) - (b6 `1 )) * ((b3 `2 ) - (b4 `2 ))) = 0. c1 & (((b3 `1 ) - (b4 `1 )) * ((b5 `3 ) - (b6 `3 ))) - (((b5 `1 ) - (b6 `1 )) * ((b3 `3 ) - (b4 `3 ))) = 0. c1 & (((b3 `2 ) - (b4 `2 )) * ((b5 `3 ) - (b6 `3 ))) - (((b5 `2 ) - (b6 `2 )) * ((b3 `3 ) - (b4 `3 ))) = 0. c1 ) ) )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff ( b3 in 4C3 c1 & ex b4, b5, b6, b7 being Element of [:the carrier of c1,the carrier of c1,the carrier of c1:] st
( b3 = [b4,b5,b6,b7] & (((b4 `1 ) - (b5 `1 )) * ((b6 `2 ) - (b7 `2 ))) - (((b6 `1 ) - (b7 `1 )) * ((b4 `2 ) - (b5 `2 ))) = 0. c1 & (((b4 `1 ) - (b5 `1 )) * ((b6 `3 ) - (b7 `3 ))) - (((b6 `1 ) - (b7 `1 )) * ((b4 `3 ) - (b5 `3 ))) = 0. c1 & (((b4 `2 ) - (b5 `2 )) * ((b6 `3 ) - (b7 `3 ))) - (((b6 `2 ) - (b7 `2 )) * ((b4 `3 ) - (b5 `3 ))) = 0. c1 ) ) ) ) & ( for b3 being set holds
( b3 in b2 iff ( b3 in 4C3 c1 & ex b4, b5, b6, b7 being Element of [:the carrier of c1,the carrier of c1,the carrier of c1:] st
( b3 = [b4,b5,b6,b7] & (((b4 `1 ) - (b5 `1 )) * ((b6 `2 ) - (b7 `2 ))) - (((b6 `1 ) - (b7 `1 )) * ((b4 `2 ) - (b5 `2 ))) = 0. c1 & (((b4 `1 ) - (b5 `1 )) * ((b6 `3 ) - (b7 `3 ))) - (((b6 `1 ) - (b7 `1 )) * ((b4 `3 ) - (b5 `3 ))) = 0. c1 & (((b4 `2 ) - (b5 `2 )) * ((b6 `3 ) - (b7 `3 ))) - (((b6 `2 ) - (b7 `2 )) * ((b4 `3 ) - (b5 `3 ))) = 0. c1 ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines PRs PARSP_1:def 9 :
for b1 being Field
for b2 being set holds
( b2 = PRs b1 iff for b3 being set holds
( b3 in b2 iff ( b3 in 4C3 b1 & ex b4, b5, b6, b7 being Element of [:the carrier of b1,the carrier of b1,the carrier of b1:] st
( b3 = [b4,b5,b6,b7] & (((b4 `1 ) - (b5 `1 )) * ((b6 `2 ) - (b7 `2 ))) - (((b6 `1 ) - (b7 `1 )) * ((b4 `2 ) - (b5 `2 ))) = 0. b1 & (((b4 `1 ) - (b5 `1 )) * ((b6 `3 ) - (b7 `3 ))) - (((b6 `1 ) - (b7 `1 )) * ((b4 `3 ) - (b5 `3 ))) = 0. b1 & (((b4 `2 ) - (b5 `2 )) * ((b6 `3 ) - (b7 `3 ))) - (((b6 `2 ) - (b7 `2 )) * ((b4 `3 ) - (b5 `3 ))) = 0. b1 ) ) ) );

theorem Th8: :: PARSP_1:8
canceled;

theorem Th9: :: PARSP_1:9
canceled;

theorem Th10: :: PARSP_1:10
canceled;

theorem Th11: :: PARSP_1:11
canceled;

theorem Th12: :: PARSP_1:12
canceled;

theorem Th13: :: PARSP_1:13
for b1 being Field holds PRs b1 c= [:(C3 b1),(C3 b1),(C3 b1),(C3 b1):]
proof end;

definition
let c1 be Field;
func PR c1 -> Relation4 of C3 a1 equals :: PARSP_1:def 10
 PRs a1;
coherence
PRs c1 is Relation4 of C3 c1
proof end;
end;

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

definition
let c1 be Field;
func MPS c1 -> ParStr equals :: PARSP_1:def 11
 ParStr(# (C3 a1),(PR a1) #);
correctness
coherence
ParStr(# (C3 c1),(PR c1) #) is ParStr ;
;
end;

:: deftheorem Def11 defines MPS PARSP_1:def 11 :
for b1 being Field holds MPS b1 = ParStr(# (C3 b1),(PR b1) #);

registration
let c1 be Field;
cluster MPS a1 -> non empty strict ;
coherence
( MPS c1 is strict & not MPS c1 is empty )
proof end;
end;

theorem Th14: :: PARSP_1:14
canceled;

theorem Th15: :: PARSP_1:15
canceled;

theorem Th16: :: PARSP_1:16
for b1 being Field holds the carrier of (MPS b1) = C3 b1 ;

theorem Th17: :: PARSP_1:17
for b1 being Field holds the 4_arg_relation of (MPS b1) = PR b1 ;

theorem Th18: :: PARSP_1:18
for b1 being Field
for b2, b3, b4, b5 being Element of (MPS b1) holds
( b2,b3 '||' b4,b5 iff [b2,b3,b4,b5] in PR b1 ) by Def6;

theorem Th19: :: PARSP_1:19
for b1 being Field
for b2, b3, b4, b5 being Element of (MPS b1) holds
( [b2,b3,b4,b5] in PR b1 iff ( [b2,b3,b4,b5] in 4C3 b1 & ex b6, b7, b8, b9 being Element of [:the carrier of b1,the carrier of b1,the carrier of b1:] st
( [b2,b3,b4,b5] = [b6,b7,b8,b9] & (((b6 `1 ) - (b7 `1 )) * ((b8 `2 ) - (b9 `2 ))) - (((b8 `1 ) - (b9 `1 )) * ((b6 `2 ) - (b7 `2 ))) = 0. b1 & (((b6 `1 ) - (b7 `1 )) * ((b8 `3 ) - (b9 `3 ))) - (((b8 `1 ) - (b9 `1 )) * ((b6 `3 ) - (b7 `3 ))) = 0. b1 & (((b6 `2 ) - (b7 `2 )) * ((b8 `3 ) - (b9 `3 ))) - (((b8 `2 ) - (b9 `2 )) * ((b6 `3 ) - (b7 `3 ))) = 0. b1 ) ) ) by Def9;

theorem Th20: :: PARSP_1:20
for b1 being Field
for b2, b3, b4, b5 being Element of (MPS b1) holds
( b2,b3 '||' b4,b5 iff ( [b2,b3,b4,b5] in 4C3 b1 & ex b6, b7, b8, b9 being Element of [:the carrier of b1,the carrier of b1,the carrier of b1:] st
( [b2,b3,b4,b5] = [b6,b7,b8,b9] & (((b6 `1 ) - (b7 `1 )) * ((b8 `2 ) - (b9 `2 ))) - (((b8 `1 ) - (b9 `1 )) * ((b6 `2 ) - (b7 `2 ))) = 0. b1 & (((b6 `1 ) - (b7 `1 )) * ((b8 `3 ) - (b9 `3 ))) - (((b8 `1 ) - (b9 `1 )) * ((b6 `3 ) - (b7 `3 ))) = 0. b1 & (((b6 `2 ) - (b7 `2 )) * ((b8 `3 ) - (b9 `3 ))) - (((b8 `2 ) - (b9 `2 )) * ((b6 `3 ) - (b7 `3 ))) = 0. b1 ) ) )
proof end;

theorem Th21: :: PARSP_1:21
for b1 being Field holds the carrier of (MPS b1) = [:the carrier of b1,the carrier of b1,the carrier of b1:] ;

theorem Th22: :: PARSP_1:22
for b1 being Field
for b2, b3, b4, b5 being Element of (MPS b1) holds [b2,b3,b4,b5] in 4C3 b1 ;

theorem Th23: :: PARSP_1:23
for b1 being Field
for b2, b3, b4, b5 being Element of (MPS b1) holds
( b2,b3 '||' b4,b5 iff ex b6, b7, b8, b9 being Element of [:the carrier of b1,the carrier of b1,the carrier of b1:] st
( [b2,b3,b4,b5] = [b6,b7,b8,b9] & (((b6 `1 ) - (b7 `1 )) * ((b8 `2 ) - (b9 `2 ))) - (((b8 `1 ) - (b9 `1 )) * ((b6 `2 ) - (b7 `2 ))) = 0. b1 & (((b6 `1 ) - (b7 `1 )) * ((b8 `3 ) - (b9 `3 ))) - (((b8 `1 ) - (b9 `1 )) * ((b6 `3 ) - (b7 `3 ))) = 0. b1 & (((b6 `2 ) - (b7 `2 )) * ((b8 `3 ) - (b9 `3 ))) - (((b8 `2 ) - (b9 `2 )) * ((b6 `3 ) - (b7 `3 ))) = 0. b1 ) )
proof end;

theorem Th24: :: PARSP_1:24
for b1 being Field
for b2, b3 being Element of (MPS b1) holds b2,b3 '||' b3,b2
proof end;

theorem Th25: :: PARSP_1:25
for b1 being Field
for b2, b3, b4 being Element of (MPS b1) holds b2,b3 '||' b4,b4
proof end;

theorem Th26: :: PARSP_1:26
for b1 being Field
for b2, b3, b4, b5, b6, b7 being Element of (MPS b1) st b2,b3 '||' b4,b5 & b2,b3 '||' b6,b7 & not b4,b5 '||' b6,b7 holds
b2 = b3
proof end;

theorem Th27: :: PARSP_1:27
for b1 being Field
for b2, b3, b4 being Element of (MPS b1) st b2,b3 '||' b2,b4 holds
b3,b2 '||' b3,b4
proof end;

theorem Th28: :: PARSP_1:28
for b1 being Field
for b2, b3, b4 being Element of (MPS b1) ex b5 being Element of (MPS b1) st
( b2,b3 '||' b4,b5 & b2,b4 '||' b3,b5 )
proof end;

definition
let c1 be non empty ParStr ;
attr a1 is ParSp-like means :Def12: :: PARSP_1:def 12
for b1, b2, b3, b4, b5, b6, b7, b8 being Element of a1 holds
( b1,b2 '||' b2,b1 & b1,b2 '||' b3,b3 & ( b1,b2 '||' b5,b6 & b1,b2 '||' b7,b8 & not b5,b6 '||' b7,b8 implies b1 = b2 ) & ( b1,b2 '||' b1,b3 implies b2,b1 '||' b2,b3 ) & ex b9 being Element of a1 st
( b1,b2 '||' b3,b9 & b1,b3 '||' b2,b9 ) );
end;

:: deftheorem Def12 defines ParSp-like PARSP_1:def 12 :
for b1 being non empty ParStr holds
( b1 is ParSp-like iff for b2, b3, b4, b5, b6, b7, b8, b9 being Element of b1 holds
( b2,b3 '||' b3,b2 & b2,b3 '||' b4,b4 & ( b2,b3 '||' b6,b7 & b2,b3 '||' b8,b9 & not b6,b7 '||' b8,b9 implies b2 = b3 ) & ( b2,b3 '||' b2,b4 implies b3,b2 '||' b3,b4 ) & ex b10 being Element of b1 st
( b2,b3 '||' b4,b10 & b2,b4 '||' b3,b10 ) ) );

registration
cluster non empty strict ParSp-like ParStr ;
existence
ex b1 being non empty ParStr st
( b1 is strict & b1 is ParSp-like )
proof end;
end;

definition
mode ParSp is non empty ParSp-like ParStr ;
end;

theorem Th29: :: PARSP_1:29
canceled;

theorem Th30: :: PARSP_1:30
canceled;

theorem Th31: :: PARSP_1:31
canceled;

theorem Th32: :: PARSP_1:32
canceled;

theorem Th33: :: PARSP_1:33
canceled;

theorem Th34: :: PARSP_1:34
canceled;

theorem Th35: :: PARSP_1:35
for b1 being ParSp
for b2, b3 being Element of b1 holds b2,b3 '||' b2,b3
proof end;

theorem Th36: :: PARSP_1:36
for b1 being ParSp
for b2, b3, b4, b5 being Element of b1 st b2,b3 '||' b4,b5 holds
b4,b5 '||' b2,b3
proof end;

theorem Th37: :: PARSP_1:37
for b1 being ParSp
for b2, b3, b4 being Element of b1 holds b2,b2 '||' b3,b4
proof end;

theorem Th38: :: PARSP_1:38
for b1 being ParSp
for b2, b3, b4, b5 being Element of b1 st b2,b3 '||' b4,b5 holds
b3,b2 '||' b4,b5
proof end;

theorem Th39: :: PARSP_1:39
for b1 being ParSp
for b2, b3, b4, b5 being Element of b1 st b2,b3 '||' b4,b5 holds
b2,b3 '||' b5,b4
proof end;

theorem Th40: :: PARSP_1:40
for b1 being ParSp
for b2, b3, b4, b5 being Element of b1 st b2,b3 '||' b4,b5 holds
( b3,b2 '||' b4,b5 & b2,b3 '||' b5,b4 & b3,b2 '||' b5,b4 & b4,b5 '||' b2,b3 & b5,b4 '||' b2,b3 & b4,b5 '||' b3,b2 & b5,b4 '||' b3,b2 )
proof end;

theorem Th41: :: PARSP_1:41
for b1 being ParSp
for b2, b3, b4 being Element of b1 st b2,b3 '||' b2,b4 holds
( b2,b4 '||' b2,b3 & b3,b2 '||' b2,b4 & b2,b3 '||' b4,b2 & b2,b4 '||' b3,b2 & b3,b2 '||' b4,b2 & b4,b2 '||' b2,b3 & b4,b2 '||' b3,b2 & b3,b2 '||' b3,b4 & b2,b3 '||' b3,b4 & b3,b2 '||' b4,b3 & b3,b4 '||' b3,b2 & b2,b3 '||' b4,b3 & b4,b3 '||' b3,b2 & b3,b4 '||' b2,b3 & b4,b3 '||' b2,b3 & b4,b2 '||' b4,b3 & b2,b4 '||' b4,b3 & b4,b2 '||' b3,b4 & b2,b4 '||' b3,b4 & b4,b3 '||' b4,b2 & b3,b4 '||' b4,b2 & b4,b3 '||' b2,b4 & b3,b4 '||' b2,b4 )
proof end;

theorem Th42: :: PARSP_1:42
for b1 being ParSp
for b2, b3, b4, b5 being Element of b1 st ( b2 = b3 or b4 = b5 or ( b2 = b4 & b3 = b5 ) or ( b2 = b5 & b3 = b4 ) ) holds
b2,b3 '||' b4,b5 by Def12, Th35, Th37;

theorem Th43: :: PARSP_1:43
for b1 being ParSp
for b2, b3, b4, b5, b6, b7 being Element of b1 st b2 <> b3 & b4,b5 '||' b2,b3 & b2,b3 '||' b6,b7 holds
b4,b5 '||' b6,b7
proof end;

theorem Th44: :: PARSP_1:44
for b1 being ParSp
for b2, b3, b4 being Element of b1 st not b2,b3 '||' b2,b4 holds
( b2 <> b3 & b3 <> b4 & b4 <> b2 ) by Def12, Th35, Th37;

theorem Th45: :: PARSP_1:45
for b1 being ParSp
for b2, b3, b4, b5 being Element of b1 st not b2,b3 '||' b4,b5 holds
( b2 <> b3 & b4 <> b5 ) by Def12, Th37;

theorem Th46: :: PARSP_1:46
canceled;

theorem Th47: :: PARSP_1:47
for b1 being ParSp
for b2, b3, b4 being Element of b1 st not b2,b3 '||' b2,b4 holds
( not b2,b4 '||' b2,b3 & not b3,b2 '||' b2,b4 & not b2,b3 '||' b4,b2 & not b2,b4 '||' b3,b2 & not b3,b2 '||' b4,b2 & not b4,b2 '||' b2,b3 & not b4,b2 '||' b3,b2 & not b3,b2 '||' b3,b4 & not b2,b3 '||' b3,b4 & not b3,b2 '||' b4,b3 & not b3,b4 '||' b3,b2 & not b3,b2 '||' b4,b3 & not b4,b3 '||' b3,b2 & not b3,b4 '||' b2,b3 & not b4,b3 '||' b2,b3 & not b4,b2 '||' b4,b3 & not b2,b4 '||' b4,b3 & not b4,b2 '||' b3,b4 & not b2,b4 '||' b3,b4 & not b4,b3 '||' b4,b2 & not b3,b4 '||' b4,b2 & not b4,b3 '||' b2,b4 & not b3,b4 '||' b2,b4 )
proof end;

theorem Th48: :: PARSP_1:48
for b1 being ParSp
for b2, b3, b4, b5, b6, b7, b8, b9 being Element of b1 st not b2,b3 '||' b4,b5 & b2,b3 '||' b6,b7 & b4,b5 '||' b8,b9 & b6 <> b7 & b8 <> b9 holds
not b6,b7 '||' b8,b9
proof end;

theorem Th49: :: PARSP_1:49
for b1 being ParSp
for b2, b3, b4, b5, b6, b7 being Element of b1 st not b2,b3 '||' b2,b4 & b2,b3 '||' b5,b6 & b2,b4 '||' b5,b7 & b3,b4 '||' b6,b7 & b5 <> b6 holds
not b5,b6 '||' b5,b7
proof end;

theorem Th50: :: PARSP_1:50
for b1 being ParSp
for b2, b3, b4, b5, b6 being Element of b1 st not b2,b3 '||' b2,b4 & b2,b4 '||' b5,b6 & b3,b4 '||' b5,b6 holds
b5 = b6
proof end;

theorem Th51: :: PARSP_1:51
for b1 being ParSp
for b2, b3, b4, b5 being Element of b1 st not b2,b3 '||' b2,b4 & b2,b4 '||' b2,b5 & b3,b4 '||' b3,b5 holds
b4 = b5
proof end;

theorem Th52: :: PARSP_1:52
for b1 being ParSp
for b2, b3, b4, b5, b6, b7, b8 being Element of b1 st not b2,b3 '||' b2,b4 & b2,b3 '||' b5,b6 & b2,b4 '||' b5,b7 & b2,b4 '||' b5,b8 & b3,b4 '||' b6,b7 & b3,b4 '||' b6,b8 holds
b7 = b8
proof end;

theorem Th53: :: PARSP_1:53
for b1 being ParSp
for b2, b3, b4, b5 being Element of b1 st b2,b3 '||' b2,b4 & b2,b3 '||' b2,b5 holds
b2,b3 '||' b4,b5
proof end;

theorem Th54: :: PARSP_1:54
for b1 being ParSp st ( for b2, b3 being Element of b1 holds b2 = b3 ) holds
for b2, b3, b4, b5 being Element of b1 holds b2,b3 '||' b4,b5
proof end;

theorem Th55: :: PARSP_1:55
for b1 being ParSp st ex b2, b3 being Element of b1 st
( b2 <> b3 & ( for b4 being Element of b1 holds b2,b3 '||' b2,b4 ) ) holds
for b2, b3, b4, b5 being Element of b1 holds b2,b3 '||' b4,b5
proof end;

theorem Th56: :: PARSP_1:56
for b1 being ParSp
for b2, b3, b4, b5, b6 being Element of b1 st not b2,b3 '||' b2,b4 & b5 <> b6 & b5,b6 '||' b5,b2 & b5,b6 '||' b5,b3 holds
not b5,b6 '||' b5,b4
proof end;