:: Parallelity Spaces :: by Eugeniusz Kusak, Wojciech Leo\'nczuk and Micha{\l} Muzalewski :: :: Received November 23, 1989 :: Copyright (c) 1990-2012 Association of Mizar Users begin Lm1: for F being non empty right_complementable add-associative right_zeroed addLoopStr for a, b being Element of F holds - (a - b) = b - a proofend; Lm2: for F being Field for a, b, c, d being Element of F holds ((a - b) * (c - d)) - ((b - a) * (d - c)) = 0. F proofend; Lm3: for F being Field for a, b, c, d being Element of F holds (a * (b - b)) - ((c - c) * d) = 0. F proofend; Lm4: for F being Field for a, e, d, b, c, h being Element of F st a <> 0. F & (a * e) - (d * b) = 0. F & (a * c) - (h * b) = 0. F holds (d * c) - (h * e) = 0. F proofend; Lm5: for F being Field for a, b, c, d being Element of F st (a * b) - (c * d) = 0. F holds (d * c) - (b * a) = 0. F proofend; Lm6: for F being Field for b, a, e, d, c, h being Element of F st b <> 0. F & (a * e) - (d * b) = 0. F & (a * c) - (h * b) = 0. F holds (d * c) - (h * e) = 0. F proofend; Lm7: for F being Field for c, d, a, b being Element of F holds (c * d) * (a * b) = ((a * c) * d) * b proofend; Lm8: for F being Field for a, b, c, d, f, g being Element of F st (a * b) - (c * d) = 0. F holds (((a * f) * g) * b) - (((c * f) * g) * d) = 0. F proofend; Lm9: for F being Field for a, b, c, d being Element of F holds (a - b) * (c - d) = (a * c) + ((- (a * d)) + (- (b * (c - d)))) proofend; Lm10: for F being Field for a, b, c, d being Element of F holds (a + b) + (c + d) = (a + (b + c)) + d proofend; Lm11: for F being non empty right_complementable add-associative right_zeroed addLoopStr for a, b, c being Element of F holds (b + a) - (c + a) = b - c proofend; Lm12: for F being non empty right_complementable add-associative right_zeroed addLoopStr for a, b being Element of F holds a + b = - ((- b) + (- a)) proofend; Lm13: for F being Field for a, b, c, d, e, f being Element of F st ((a - b) * (c - d)) - ((a - e) * (c - f)) = 0. F holds ((b - a) * (f - d)) - ((b - e) * (f - c)) = 0. F proofend; Lm14: for F being Field for a, b, c being Element of F holds a - ((a + b) + (- c)) = c - b proofend; Lm15: for F being Field for a, b, c, h, g, e being Element of F holds ((a - b) * (c - ((c + h) + (- g)))) - ((e - ((e + b) + (- a))) * (g - h)) = 0. F proofend; deffunc H1( Field) -> set = [: the carrier of $1, the carrier of $1, the carrier of $1:]; definition let F be Field; func c3add F -> BinOp of [: the carrier of F, the carrier of F, the carrier of F:] means :Def1: :: PARSP_1:def 1 for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds it . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))]; existence ex b1 being BinOp of [: the carrier of F, the carrier of F, the carrier of F:] st for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b1 . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] proofend; uniqueness for b1, b2 being BinOp of [: the carrier of F, the carrier of F, the carrier of F:] st ( for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b1 . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] ) & ( for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b2 . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines c3add PARSP_1:def_1_:_ for F being Field for b2 being BinOp of [: the carrier of F, the carrier of F, the carrier of F:] holds ( b2 = c3add F iff for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b2 . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] ); definition let F be Field; let x, y be Element of [: the carrier of F, the carrier of F, the carrier of F:]; funcx + y -> Element of [: the carrier of F, the carrier of F, the carrier of F:] equals :: PARSP_1:def 2 (c3add F) . (x,y); coherence (c3add F) . (x,y) is Element of [: the carrier of F, the carrier of F, the carrier of F:] ; end; :: deftheorem defines + PARSP_1:def_2_:_ for F being Field for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds x + y = (c3add F) . (x,y); theorem :: PARSP_1:1 for F being Field for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds x + y = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] by Def1; theorem Th2: :: PARSP_1:2 for F being Field for a, b, c, f, g, h being Element of F holds [a,b,c] + [f,g,h] = [(a + f),(b + g),(c + h)] proofend; definition let F be Field; func c3compl F -> UnOp of [: the carrier of F, the carrier of F, the carrier of F:] means :Def3: :: PARSP_1:def 3 for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds it . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))]; existence ex b1 being UnOp of [: the carrier of F, the carrier of F, the carrier of F:] st for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b1 . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))] proofend; uniqueness for b1, b2 being UnOp of [: the carrier of F, the carrier of F, the carrier of F:] st ( for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b1 . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))] ) & ( for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b2 . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))] ) holds b1 = b2 proofend; end; :: deftheorem Def3 defines c3compl PARSP_1:def_3_:_ for F being Field for b2 being UnOp of [: the carrier of F, the carrier of F, the carrier of F:] holds ( b2 = c3compl F iff for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b2 . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))] ); definition let F be Field; let x be Element of [: the carrier of F, the carrier of F, the carrier of F:]; func - x -> Element of [: the carrier of F, the carrier of F, the carrier of F:] equals :: PARSP_1:def 4 (c3compl F) . x; coherence (c3compl F) . x is Element of [: the carrier of F, the carrier of F, the carrier of F:] ; end; :: deftheorem defines - PARSP_1:def_4_:_ for F being Field for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds - x = (c3compl F) . x; theorem :: PARSP_1:3 for F being Field for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds - x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))] by Def3; definition let S be set ; mode Relation4 of S -> set means :Def5: :: PARSP_1:def 5 it c= [:S,S,S,S:]; existence ex b1 being set st b1 c= [:S,S,S,S:] ; end; :: deftheorem Def5 defines Relation4 PARSP_1:def_5_:_ for S, b2 being set holds ( b2 is Relation4 of S iff b2 c= [:S,S,S,S:] ); definition attrc1 is strict ; struct ParStr -> 1-sorted ; aggrParStr(# carrier, 4_arg_relation #) -> ParStr ; sel 4_arg_relation c1 -> Relation4 of the carrier of c1; end; registration cluster non empty for ParStr ; existence not for b1 being ParStr holds b1 is empty proofend; end; definition let PS be non empty ParStr ; let a, b, c, d be Element of PS; preda,b '||' c,d means :Def6: :: PARSP_1:def 6 [a,b,c,d] in the 4_arg_relation of PS; end; :: deftheorem Def6 defines '||' PARSP_1:def_6_:_ for PS being non empty ParStr for a, b, c, d being Element of PS holds ( a,b '||' c,d iff [a,b,c,d] in the 4_arg_relation of PS ); definition let F be Field; func C_3 F -> set equals :: PARSP_1:def 7 [: the carrier of F, the carrier of F, the carrier of F:]; coherence [: the carrier of F, the carrier of F, the carrier of F:] is set ; end; :: deftheorem defines C_3 PARSP_1:def_7_:_ for F being Field holds C_3 F = [: the carrier of F, the carrier of F, the carrier of F:]; registration let F be Field; cluster C_3 F -> non empty ; coherence not C_3 F is empty ; end; definition let F be Field; func 4C_3 F -> set equals :: PARSP_1:def 8 [:(C_3 F),(C_3 F),(C_3 F),(C_3 F):]; coherence [:(C_3 F),(C_3 F),(C_3 F),(C_3 F):] is set ; end; :: deftheorem defines 4C_3 PARSP_1:def_8_:_ for F being Field holds 4C_3 F = [:(C_3 F),(C_3 F),(C_3 F),(C_3 F):]; registration let F be Field; cluster 4C_3 F -> non empty ; coherence not 4C_3 F is empty ; end; definition let F be Field; func PRs F -> set means :Def9: :: PARSP_1:def 9 for x being set holds ( x in it iff ( x in 4C_3 F & ex a, b, c, d being Element of [: the carrier of F, the carrier of F, the carrier of F:] st ( x = [a,b,c,d] & (((a `1_3) - (b `1_3)) * ((c `2_3) - (d `2_3))) - (((c `1_3) - (d `1_3)) * ((a `2_3) - (b `2_3))) = 0. F & (((a `1_3) - (b `1_3)) * ((c `3_3) - (d `3_3))) - (((c `1_3) - (d `1_3)) * ((a `3_3) - (b `3_3))) = 0. F & (((a `2_3) - (b `2_3)) * ((c `3_3) - (d `3_3))) - (((c `2_3) - (d `2_3)) * ((a `3_3) - (b `3_3))) = 0. F ) ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ( x in 4C_3 F & ex a, b, c, d being Element of [: the carrier of F, the carrier of F, the carrier of F:] st ( x = [a,b,c,d] & (((a `1_3) - (b `1_3)) * ((c `2_3) - (d `2_3))) - (((c `1_3) - (d `1_3)) * ((a `2_3) - (b `2_3))) = 0. F & (((a `1_3) - (b `1_3)) * ((c `3_3) - (d `3_3))) - (((c `1_3) - (d `1_3)) * ((a `3_3) - (b `3_3))) = 0. F & (((a `2_3) - (b `2_3)) * ((c `3_3) - (d `3_3))) - (((c `2_3) - (d `2_3)) * ((a `3_3) - (b `3_3))) = 0. F ) ) ) proofend; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x in 4C_3 F & ex a, b, c, d being Element of [: the carrier of F, the carrier of F, the carrier of F:] st ( x = [a,b,c,d] & (((a `1_3) - (b `1_3)) * ((c `2_3) - (d `2_3))) - (((c `1_3) - (d `1_3)) * ((a `2_3) - (b `2_3))) = 0. F & (((a `1_3) - (b `1_3)) * ((c `3_3) - (d `3_3))) - (((c `1_3) - (d `1_3)) * ((a `3_3) - (b `3_3))) = 0. F & (((a `2_3) - (b `2_3)) * ((c `3_3) - (d `3_3))) - (((c `2_3) - (d `2_3)) * ((a `3_3) - (b `3_3))) = 0. F ) ) ) ) & ( for x being set holds ( x in b2 iff ( x in 4C_3 F & ex a, b, c, d being Element of [: the carrier of F, the carrier of F, the carrier of F:] st ( x = [a,b,c,d] & (((a `1_3) - (b `1_3)) * ((c `2_3) - (d `2_3))) - (((c `1_3) - (d `1_3)) * ((a `2_3) - (b `2_3))) = 0. F & (((a `1_3) - (b `1_3)) * ((c `3_3) - (d `3_3))) - (((c `1_3) - (d `1_3)) * ((a `3_3) - (b `3_3))) = 0. F & (((a `2_3) - (b `2_3)) * ((c `3_3) - (d `3_3))) - (((c `2_3) - (d `2_3)) * ((a `3_3) - (b `3_3))) = 0. F ) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def9 defines PRs PARSP_1:def_9_:_ for F being Field for b2 being set holds ( b2 = PRs F iff for x being set holds ( x in b2 iff ( x in 4C_3 F & ex a, b, c, d being Element of [: the carrier of F, the carrier of F, the carrier of F:] st ( x = [a,b,c,d] & (((a `1_3) - (b `1_3)) * ((c `2_3) - (d `2_3))) - (((c `1_3) - (d `1_3)) * ((a `2_3) - (b `2_3))) = 0. F & (((a `1_3) - (b `1_3)) * ((c `3_3) - (d `3_3))) - (((c `1_3) - (d `1_3)) * ((a `3_3) - (b `3_3))) = 0. F & (((a `2_3) - (b `2_3)) * ((c `3_3) - (d `3_3))) - (((c `2_3) - (d `2_3)) * ((a `3_3) - (b `3_3))) = 0. F ) ) ) ); theorem Th4: :: PARSP_1:4 for F being Field holds PRs F c= [:(C_3 F),(C_3 F),(C_3 F),(C_3 F):] proofend; definition let F be Field; func PR F -> Relation4 of C_3 F equals :: PARSP_1:def 10 PRs F; coherence PRs F is Relation4 of C_3 F proofend; end; :: deftheorem defines PR PARSP_1:def_10_:_ for F being Field holds PR F = PRs F; definition let F be Field; func MPS F -> ParStr equals :: PARSP_1:def 11 ParStr(# (C_3 F),(PR F) #); correctness coherence ParStr(# (C_3 F),(PR F) #) is ParStr ; ; end; :: deftheorem defines MPS PARSP_1:def_11_:_ for F being Field holds MPS F = ParStr(# (C_3 F),(PR F) #); registration let F be Field; cluster MPS F -> non empty strict ; coherence ( MPS F is strict & not MPS F is empty ) ; end; theorem :: PARSP_1:5 for F being Field holds the carrier of (MPS F) = C_3 F ; theorem :: PARSP_1:6 for F being Field holds the 4_arg_relation of (MPS F) = PR F ; theorem :: PARSP_1:7 for F being Field for a, b, c, d being Element of (MPS F) holds ( a,b '||' c,d iff [a,b,c,d] in PR F ) by Def6; theorem :: PARSP_1:8 for F being Field for a, b, c, d being Element of (MPS F) holds ( [a,b,c,d] in PR F iff ( [a,b,c,d] in 4C_3 F & ex e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] st ( [a,b,c,d] = [e,f,g,h] & (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F & (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F ) ) ) by Def9; theorem Th9: :: PARSP_1:9 for F being Field for a, b, c, d being Element of (MPS F) holds ( a,b '||' c,d iff ( [a,b,c,d] in 4C_3 F & ex e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] st ( [a,b,c,d] = [e,f,g,h] & (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F & (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F ) ) ) proofend; theorem :: PARSP_1:10 for F being Field holds the carrier of (MPS F) = [: the carrier of F, the carrier of F, the carrier of F:] ; theorem :: PARSP_1:11 for F being Field for a, b, c, d being Element of (MPS F) holds [a,b,c,d] in 4C_3 F ; theorem Th12: :: PARSP_1:12 for F being Field for a, b, c, d being Element of (MPS F) holds ( a,b '||' c,d iff ex e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] st ( [a,b,c,d] = [e,f,g,h] & (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F & (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F ) ) proofend; theorem Th13: :: PARSP_1:13 for F being Field for a, b being Element of (MPS F) holds a,b '||' b,a proofend; theorem Th14: :: PARSP_1:14 for F being Field for a, b, c being Element of (MPS F) holds a,b '||' c,c proofend; theorem Th15: :: PARSP_1:15 for F being Field for a, b, p, q, r, s being Element of (MPS F) st a,b '||' p,q & a,b '||' r,s & not p,q '||' r,s holds a = b proofend; theorem Th16: :: PARSP_1:16 for F being Field for a, b, c being Element of (MPS F) st a,b '||' a,c holds b,a '||' b,c proofend; theorem Th17: :: PARSP_1:17 for F being Field for a, b, c being Element of (MPS F) ex d being Element of (MPS F) st ( a,b '||' c,d & a,c '||' b,d ) proofend; :: :: 3. DEFINITION OF PARALLELITY SPACE :: definition let IT be non empty ParStr ; attrIT is ParSp-like means :Def12: :: PARSP_1:def 12 for a, b, c, d, p, q, r, s being Element of IT holds ( a,b '||' b,a & a,b '||' c,c & ( a,b '||' p,q & a,b '||' r,s & not p,q '||' r,s implies a = b ) & ( a,b '||' a,c implies b,a '||' b,c ) & ex x being Element of IT st ( a,b '||' c,x & a,c '||' b,x ) ); end; :: deftheorem Def12 defines ParSp-like PARSP_1:def_12_:_ for IT being non empty ParStr holds ( IT is ParSp-like iff for a, b, c, d, p, q, r, s being Element of IT holds ( a,b '||' b,a & a,b '||' c,c & ( a,b '||' p,q & a,b '||' r,s & not p,q '||' r,s implies a = b ) & ( a,b '||' a,c implies b,a '||' b,c ) & ex x being Element of IT st ( a,b '||' c,x & a,c '||' b,x ) ) ); registration cluster non empty strict ParSp-like for ParStr ; existence ex b1 being non empty ParStr st ( b1 is strict & b1 is ParSp-like ) proofend; end; definition mode ParSp is non empty ParSp-like ParStr ; end; theorem Th18: :: PARSP_1:18 for PS being ParSp for a, b being Element of PS holds a,b '||' a,b proofend; theorem Th19: :: PARSP_1:19 for PS being ParSp for a, b, c, d being Element of PS st a,b '||' c,d holds c,d '||' a,b proofend; theorem Th20: :: PARSP_1:20 for PS being ParSp for a, b, c being Element of PS holds a,a '||' b,c proofend; theorem Th21: :: PARSP_1:21 for PS being ParSp for a, b, c, d being Element of PS st a,b '||' c,d holds b,a '||' c,d proofend; theorem Th22: :: PARSP_1:22 for PS being ParSp for a, b, c, d being Element of PS st a,b '||' c,d holds a,b '||' d,c proofend; theorem Th23: :: PARSP_1:23 for PS being ParSp for a, b, c, d being Element of PS st a,b '||' c,d holds ( b,a '||' c,d & a,b '||' d,c & b,a '||' d,c & c,d '||' a,b & d,c '||' a,b & c,d '||' b,a & d,c '||' b,a ) proofend; theorem Th24: :: PARSP_1:24 for PS being ParSp for a, b, c being Element of PS st a,b '||' a,c holds ( a,c '||' a,b & b,a '||' a,c & a,b '||' c,a & a,c '||' b,a & b,a '||' c,a & c,a '||' a,b & c,a '||' b,a & b,a '||' b,c & a,b '||' b,c & b,a '||' c,b & b,c '||' b,a & a,b '||' c,b & c,b '||' b,a & b,c '||' a,b & c,b '||' a,b & c,a '||' c,b & a,c '||' c,b & c,a '||' b,c & a,c '||' b,c & c,b '||' c,a & b,c '||' c,a & c,b '||' a,c & b,c '||' a,c ) proofend; theorem :: PARSP_1:25 for PS being ParSp for a, b, c, d being Element of PS st ( a = b or c = d or ( a = c & b = d ) or ( a = d & b = c ) ) holds a,b '||' c,d by Def12, Th18, Th20; theorem Th26: :: PARSP_1:26 for PS being ParSp for a, b, p, q, r, s being Element of PS st a <> b & p,q '||' a,b & a,b '||' r,s holds p,q '||' r,s proofend; theorem :: PARSP_1:27 for PS being ParSp for a, b, c being Element of PS st not a,b '||' a,c holds ( a <> b & b <> c & c <> a ) by Def12, Th18, Th20; theorem :: PARSP_1:28 for PS being ParSp for a, b, c, d being Element of PS st not a,b '||' c,d holds ( a <> b & c <> d ) by Def12, Th20; theorem Th29: :: PARSP_1:29 for PS being ParSp for a, b, c being Element of PS st not a,b '||' a,c holds ( not a,c '||' a,b & not b,a '||' a,c & not a,b '||' c,a & not a,c '||' b,a & not b,a '||' c,a & not c,a '||' a,b & not c,a '||' b,a & not b,a '||' b,c & not a,b '||' b,c & not b,a '||' c,b & not b,c '||' b,a & not b,a '||' c,b & not c,b '||' b,a & not b,c '||' a,b & not c,b '||' a,b & not c,a '||' c,b & not a,c '||' c,b & not c,a '||' b,c & not a,c '||' b,c & not c,b '||' c,a & not b,c '||' c,a & not c,b '||' a,c & not b,c '||' a,c ) proofend; theorem Th30: :: PARSP_1:30 for PS being ParSp for a, b, c, d, p, q, r, s being Element of PS st not a,b '||' c,d & a,b '||' p,q & c,d '||' r,s & p <> q & r <> s holds not p,q '||' r,s proofend; theorem Th31: :: PARSP_1:31 for PS being ParSp for a, b, c, p, q, r being Element of PS st not a,b '||' a,c & a,b '||' p,q & a,c '||' p,r & b,c '||' q,r & p <> q holds not p,q '||' p,r proofend; theorem Th32: :: PARSP_1:32 for PS being ParSp for a, b, c, p, r being Element of PS st not a,b '||' a,c & a,c '||' p,r & b,c '||' p,r holds p = r proofend; theorem Th33: :: PARSP_1:33 for PS being ParSp for p, q, r, s being Element of PS st not p,q '||' p,r & p,r '||' p,s & q,r '||' q,s holds r = s proofend; theorem :: PARSP_1:34 for PS being ParSp for a, b, c, p, q, r, s being Element of PS st not a,b '||' a,c & a,b '||' p,q & a,c '||' p,r & a,c '||' p,s & b,c '||' q,r & b,c '||' q,s holds r = s proofend; theorem Th35: :: PARSP_1:35 for PS being ParSp for a, b, c, d being Element of PS st a,b '||' a,c & a,b '||' a,d holds a,b '||' c,d proofend; theorem :: PARSP_1:36 for PS being ParSp st ( for a, b being Element of PS holds a = b ) holds for p, q, r, s being Element of PS holds p,q '||' r,s proofend; theorem :: PARSP_1:37 for PS being ParSp st ex a, b being Element of PS st ( a <> b & ( for c being Element of PS holds a,b '||' a,c ) ) holds for p, q, r, s being Element of PS holds p,q '||' r,s proofend; theorem :: PARSP_1:38 for PS being ParSp for a, b, c, p, q being Element of PS st not a,b '||' a,c & p <> q & p,q '||' p,a & p,q '||' p,b holds not p,q '||' p,c proofend;