:: by Eugeniusz Kusak and Wojciech Leo\'nczuk

::

:: Received March 23, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

Lm1: for F being non empty right_complementable add-associative right_zeroed addLoopStr

for a, b being Element of F st a - b = 0. F holds

a = b

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

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

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

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

Lm5: for F being Field

for K, L, R being Element of F holds (K - L) - (R - L) = K - R

proof end;

Lm6: for F being Field

for K, L, M, N, 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 end;

Lm7: for F being Field

for K, L, M, N being Element of F st K - L = N - M holds

M = (L + N) - K

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

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

Lm8: for F being Field

for K, L, R being Element of F st (L * K) - (L * R) = R + K holds

(L - (1_ F)) * K = (L + (1_ F)) * R

proof end;

Lm9: for F being Field

for K, L, 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 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 end;

theorem Th7: :: PARSP_2:7

for F being Field

for a, b, c, 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

for a, b, c, 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 end;

theorem Th8: :: PARSP_2:8

for F being Field

for a, b, c, p, 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

for a, b, c, p, 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 end;

:: 2. DEFINITION OF A FANO-DESARGUES SPACE

definition

let IT be ParSp;

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

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

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

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

:: 3. AXIOMS OF A FANO-DESARGUES PARALLELITY SPACE

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

for p, q being Element of FdSp st p <> q holds

ex r being Element of FdSp st not p,q '||' p,r

proof end;

:: deftheorem defines are_collinear PARSP_2:def 2 :

for FdSp being FanodesSp

for a, b, c being Element of FdSp holds

( a,b,c are_collinear iff a,b '||' a,c );

for FdSp being FanodesSp

for a, b, c being Element of FdSp holds

( a,b,c are_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 are_collinear holds

( a,c,b are_collinear & c,b,a are_collinear & b,a,c are_collinear & b,c,a are_collinear & c,a,b are_collinear ) by PARSP_1:24;

for a, b, c being Element of FdSp st a,b,c are_collinear holds

( a,c,b are_collinear & c,b,a are_collinear & b,a,c are_collinear & b,c,a are_collinear & c,a,b are_collinear ) by PARSP_1:24;

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 are_collinear & a,b '||' p,q & a,c '||' p,r & p <> q & p <> r holds

not p,q,r are_collinear by PARSP_1:30;

for a, b, c, p, q, r being Element of FdSp st not a,b,c are_collinear & a,b '||' p,q & a,c '||' p,r & p <> q & p <> r holds

not p,q,r are_collinear by PARSP_1:30;

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 are_collinear by PARSP_1:25;

for a, b, c being Element of FdSp st ( a = b or b = c or c = a ) holds

a,b,c are_collinear by PARSP_1:25;

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 are_collinear & a,b,q are_collinear & a,b,r are_collinear holds

p,q,r are_collinear

for a, b, p, q, r being Element of FdSp st a <> b & a,b,p are_collinear & a,b,q are_collinear & a,b,r are_collinear holds

p,q,r are_collinear

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

for p, q being Element of FdSp st p <> q holds

ex r being Element of FdSp st not p,q,r are_collinear

proof end;

theorem Th15: :: PARSP_2:15

for FdSp being FanodesSp

for a, b, c, d being Element of FdSp st a,b,c are_collinear & a,b,d are_collinear holds

a,b '||' c,d by PARSP_1:35;

for a, b, c, d being Element of FdSp st a,b,c are_collinear & a,b,d are_collinear holds

a,b '||' c,d by PARSP_1:35;

theorem Th16: :: PARSP_2:16

for FdSp being FanodesSp

for a, b, c, d being Element of FdSp st not a,b,c are_collinear & a,b '||' c,d holds

not a,b,d are_collinear

for a, b, c, d being Element of FdSp st not a,b,c are_collinear & a,b '||' c,d holds

not a,b,d are_collinear

proof 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 are_collinear & a,b '||' c,d & c <> d & a,b,x are_collinear holds

not c,d,x are_collinear by Th16, PARSP_1:26;

for a, b, c, d, x being Element of FdSp st not a,b,c are_collinear & a,b '||' c,d & c <> d & a,b,x are_collinear holds

not c,d,x are_collinear by Th16, PARSP_1:26;

theorem :: PARSP_2:18

for FdSp being FanodesSp

for a, b, o, x being Element of FdSp holds

( o,a,b are_collinear or not o,a,x are_collinear or not o,b,x are_collinear or o = x )

for a, b, o, x being Element of FdSp holds

( o,a,b are_collinear or not o,a,x are_collinear or not o,b,x are_collinear or o = x )

proof end;

theorem :: PARSP_2:19

for FdSp being FanodesSp

for a, b, p, q, o being Element of FdSp st o <> a & o <> b & o,a,b are_collinear & o,a,p are_collinear & o,b,q are_collinear holds

a,b '||' p,q

for a, b, p, q, o being Element of FdSp st o <> a & o <> b & o,a,b are_collinear & o,a,p are_collinear & o,b,q are_collinear holds

a,b '||' p,q

proof 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 are_collinear & a,b,q are_collinear & c,d,p are_collinear & c,d,q are_collinear holds

p = q

for a, b, c, d, p, q being Element of FdSp st not a,b '||' c,d & a,b,p are_collinear & a,b,q are_collinear & c,d,p are_collinear & c,d,q are_collinear holds

p = q

proof end;

theorem :: PARSP_2:21

for FdSp being FanodesSp

for a, b, c, d being Element of FdSp st a <> b & a,b,c are_collinear & a,b '||' c,d holds

a,c '||' b,d

for a, b, c, d being Element of FdSp st a <> b & a,b,c are_collinear & a,b '||' c,d holds

a,c '||' b,d

proof end;

theorem :: PARSP_2:22

for FdSp being FanodesSp

for a, b, c, d being Element of FdSp st a <> b & a,b,c are_collinear & a,b '||' c,d holds

c,b '||' c,d

for a, b, c, d being Element of FdSp st a <> b & a,b,c are_collinear & a,b '||' c,d holds

c,b '||' c,d

proof end;

theorem :: PARSP_2:23

for FdSp being FanodesSp

for a, b, c, p, q, o being Element of FdSp st not o,a,c are_collinear & o,a,b are_collinear & o,c,p are_collinear & o,c,q are_collinear & a,c '||' b,p & a,c '||' b,q holds

p = q by PARSP_1:34;

for a, b, c, p, q, o being Element of FdSp st not o,a,c are_collinear & o,a,b are_collinear & o,c,p are_collinear & o,c,q are_collinear & a,c '||' b,p & a,c '||' b,q holds

p = q by PARSP_1:34;

theorem :: PARSP_2:24

for FdSp being FanodesSp

for a, b, c, d being Element of FdSp st a <> b & a,b,c are_collinear & a,b,d are_collinear holds

a,c,d are_collinear by PARSP_1:def 12;

for a, b, c, d being Element of FdSp st a <> b & a,b,c are_collinear & a,b,d are_collinear holds

a,c,d are_collinear by PARSP_1:def 12;

theorem :: PARSP_2:25

for FdSp being FanodesSp

for a, b, c, d being Element of FdSp st a,b,c are_collinear & a,c,d are_collinear & a <> c holds

b,c,d are_collinear

for a, b, c, d being Element of FdSp st a,b,c are_collinear & a,c,d are_collinear & a <> c holds

b,c,d are_collinear

proof end;

definition

let FdSp be FanodesSp;

let a, b, c, d be Element of FdSp;

end;
let a, b, c, d be Element of FdSp;

pred parallelogram a,b,c,d means :: PARSP_2:def 3

( not a,b,c are_collinear & a,b '||' c,d & a,c '||' b,d );

( not a,b,c are_collinear & a,b '||' c,d & a,c '||' b,d );

:: deftheorem 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 are_collinear & a,b '||' c,d & a,c '||' b,d ) );

for FdSp being FanodesSp

for a, b, c, d being Element of FdSp holds

( parallelogram a,b,c,d iff ( not a,b,c are_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 )

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 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 are_collinear & not b,a,d are_collinear & not c,d,a are_collinear & not d,c,b are_collinear )

for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds

( not a,b,c are_collinear & not b,a,d are_collinear & not c,d,a are_collinear & not d,c,b are_collinear )

proof 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 are_collinear & not b,a,d are_collinear & not c,d,a are_collinear & not d,c,b are_collinear & not a,c,b are_collinear & not b,a,c are_collinear & not b,c,a are_collinear & not c,a,b are_collinear & not c,b,a are_collinear & not b,d,a are_collinear & not a,b,d are_collinear & not a,d,b are_collinear & not d,a,b are_collinear & not d,b,a are_collinear & not c,a,d are_collinear & not a,c,d are_collinear & not a,d,c are_collinear & not d,a,c are_collinear & not d,c,a are_collinear & not d,b,c are_collinear & not b,c,d are_collinear & not b,d,c are_collinear & not c,b,d are_collinear & not c,d,b are_collinear )

for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds

( not a,b,c are_collinear & not b,a,d are_collinear & not c,d,a are_collinear & not d,c,b are_collinear & not a,c,b are_collinear & not b,a,c are_collinear & not b,c,a are_collinear & not c,a,b are_collinear & not c,b,a are_collinear & not b,d,a are_collinear & not a,b,d are_collinear & not a,d,b are_collinear & not d,a,b are_collinear & not d,b,a are_collinear & not c,a,d are_collinear & not a,c,d are_collinear & not a,d,c are_collinear & not d,a,c are_collinear & not d,c,a are_collinear & not d,b,c are_collinear & not b,c,d are_collinear & not b,d,c are_collinear & not c,b,d are_collinear & not c,d,b are_collinear )

proof 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 are_collinear or not c,d,x are_collinear )

for a, b, c, d, x being Element of FdSp holds

( not parallelogram a,b,c,d or not a,b,x are_collinear or not c,d,x are_collinear )

proof 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 by Th28;

for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds

parallelogram a,c,b,d by Th28;

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 by PARSP_1:23, Th28;

for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds

parallelogram c,d,a,b by PARSP_1:23, Th28;

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 by PARSP_1:23, Th28;

for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds

parallelogram b,a,d,c by PARSP_1:23, Th28;

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 )

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

theorem Th34: :: PARSP_2:34

for FdSp being FanodesSp

for a, b, c being Element of FdSp st not a,b,c are_collinear holds

ex d being Element of FdSp st parallelogram a,b,c,d

for a, b, c being Element of FdSp st not a,b,c are_collinear holds

ex d being Element of FdSp st parallelogram a,b,c,d

proof 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

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

for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds

not a,d '||' b,c

proof 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 by Th36;

for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds

not parallelogram a,b,d,c by Th36;

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 are_collinear & c <> a & c <> b )

for a, b being Element of FdSp st a <> b holds

ex c being Element of FdSp st

( a,b,c are_collinear & c <> a & c <> b )

proof end;

theorem Th39: :: PARSP_2:39

for FdSp being FanodesSp

for a, b, c, p, q, r being Element of FdSp st parallelogram a,p,b,q & parallelogram a,p,c,r holds

b,c '||' q,r

for a, b, c, p, q, r being Element of FdSp st parallelogram a,p,b,q & parallelogram a,p,c,r holds

b,c '||' q,r

proof end;

theorem Th40: :: PARSP_2:40

for FdSp being FanodesSp

for a, b, c, p, q, r being Element of FdSp st not b,q,c are_collinear & parallelogram a,p,b,q & parallelogram a,p,c,r holds

parallelogram b,q,c,r

for a, b, c, p, q, r being Element of FdSp st not b,q,c are_collinear & parallelogram a,p,b,q & parallelogram a,p,c,r holds

parallelogram b,q,c,r

proof 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 are_collinear & b <> c & parallelogram a,p,b,q & parallelogram a,p,c,r holds

parallelogram b,q,c,r

for a, b, c, p, q, r being Element of FdSp st a,b,c are_collinear & b <> c & parallelogram a,p,b,q & parallelogram a,p,c,r holds

parallelogram b,q,c,r

proof end;

theorem Th42: :: PARSP_2:42

for FdSp being FanodesSp

for a, b, c, d, p, q, r, 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

for a, b, c, d, p, q, r, 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 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

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

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

definition

let FdSp be FanodesSp;

let a, b, r, s be Element of FdSp;

end;
let a, b, r, s be Element of FdSp;

pred a,b congr r,s means :: 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 ) );

( ( a = b & r = s ) or ex p, q being Element of FdSp st

( parallelogram p,q,a,b & parallelogram p,q,r,s ) );

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

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

theorem :: PARSP_2:47

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

parallelogram a,b,c,d by Th48, Th49;

for a, b, c, d being Element of FdSp st a,b congr c,d & not a,b,c are_collinear holds

parallelogram a,b,c,d by Th48, Th49;

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

for a, b, c, d being Element of FdSp st parallelogram a,b,c,d holds

a,b congr c,d

proof 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 are_collinear & parallelogram r,s,a,b holds

parallelogram r,s,c,d

for a, b, c, d, r, s being Element of FdSp st a,b congr c,d & a,b,c are_collinear & parallelogram r,s,a,b holds

parallelogram r,s,c,d

proof 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

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

for a, b, c being Element of FdSp ex d being Element of FdSp st a,b congr c,d

proof end;

theorem :: PARSP_2:56

for FdSp being FanodesSp

for a, b, c, d, r, s being Element of FdSp st r,s congr a,b & r,s congr c,d holds

a,b congr c,d

for a, b, c, d, r, s being Element of FdSp st r,s congr a,b & r,s congr c,d holds

a,b congr c,d

proof end;

theorem :: PARSP_2:57