:: PARSP_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for F being non empty add-associative right_zeroed right_complementable LoopStr
for a, b being Element of F st a - b = 0. F holds
a = b
proof end;

Lm2: for F being non empty add-associative right_zeroed right_complementable LoopStr
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;

theorem Th1: :: PARSP_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field holds MPS F is ParSp
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 ) - (f `1 )) * ((g `2 ) - (h `2 ))) - (((g `1 ) - (h `1 )) * ((e `2 ) - (f `2 ))) = 0. F & (((e `1 ) - (f `1 )) * ((g `3 ) - (h `3 ))) - (((g `1 ) - (h `1 )) * ((e `3 ) - (f `3 ))) = 0. F & (((e `2 ) - (f `2 )) * ((g `3 ) - (h `3 ))) - (((g `2 ) - (h `2 )) * ((e `3 ) - (f `3 ))) = 0. F ) iff ( ex K being Element of F st
( K * ((e `1 ) - (f `1 )) = (g `1 ) - (h `1 ) & K * ((e `2 ) - (f `2 )) = (g `2 ) - (h `2 ) & K * ((e `3 ) - (f `3 )) = (g `3 ) - (h `3 ) ) or ( (e `1 ) - (f `1 ) = 0. F & (e `2 ) - (f `2 ) = 0. F & (e `3 ) - (f `3 ) = 0. F ) ) )
proof end;

theorem Th2: :: PARSP_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) - (f `1 )) = (g `1 ) - (h `1 ) & K * ((e `2 ) - (f `2 )) = (g `2 ) - (h `2 ) & K * ((e `3 ) - (f `3 )) = (g `3 ) - (h `3 ) ) or ( (e `1 ) - (f `1 ) = 0. F & (e `2 ) - (f `2 ) = 0. F & (e `3 ) - (f `3 ) = 0. F ) ) ) )
proof end;

theorem Th3: :: PARSP_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th4: :: PARSP_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) - (f `1 )) = L * ((e `1 ) - (g `1 )) & K * ((e `2 ) - (f `2 )) = L * ((e `2 ) - (g `2 )) & K * ((e `3 ) - (f `3 )) = L * ((e `3 ) - (g `3 )) holds
( K = 0. F & L = 0. F )
proof end;

Lm4: for F being non empty add-associative right_zeroed right_complementable LoopStr
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, 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 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 end;

theorem Th5: :: PARSP_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 = ((f `1 ) + (g `1 )) - (e `1 ) & h `2 = ((f `2 ) + (g `2 )) - (e `2 ) & h `3 = ((f `3 ) + (g `3 )) - (e `3 ) )
proof 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 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 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 Th6: :: PARSP_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field holds
not for a, b, c being Element of (MPS F) holds a,b '||' a,c
proof end;

theorem Th7: :: PARSP_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th8: :: PARSP_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let IT be ParSp;
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 ) );
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 strict FanodesSp-like ParStr ;
existence
ex b1 being ParSp st
( b1 is strict & b1 is FanodesSp-like )
proof end;
end;

definition
mode FanodesSp is FanodesSp-like ParSp;
end;

theorem :: PARSP_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARSP_2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARSP_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARSP_2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th13: :: PARSP_2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let FdSp be FanodesSp;
let a, b, c be Element of FdSp;
pred a,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 :: PARSP_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th15: :: PARSP_2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PARSP_2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th17: :: PARSP_2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th18: :: PARSP_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th19: :: PARSP_2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th20: :: PARSP_2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th21: :: PARSP_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th22: :: PARSP_2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th23: :: PARSP_2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PARSP_2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PARSP_2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PARSP_2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PARSP_2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PARSP_2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PARSP_2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PARSP_2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PARSP_2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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 :: PARSP_2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARSP_2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th34: :: PARSP_2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th35: :: PARSP_2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th36: :: PARSP_2:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th37: :: PARSP_2:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th38: :: PARSP_2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th39: :: PARSP_2:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th40: :: PARSP_2:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th41: :: PARSP_2:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th42: :: PARSP_2:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th43: :: PARSP_2:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th44: :: PARSP_2:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th45: :: PARSP_2:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th46: :: PARSP_2:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th47: :: PARSP_2:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th48: :: PARSP_2:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th49: :: PARSP_2:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th50: :: PARSP_2:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th51: :: PARSP_2:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PARSP_2:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let FdSp be FanodesSp;
let a, b, r, s be Element of FdSp;
pred a,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 :: PARSP_2:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARSP_2:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th55: :: PARSP_2:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FdSp being FanodesSp
for a, b, c being Element of FdSp st a,a congr b,c holds
b = c
proof end;

theorem :: PARSP_2:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FdSp being FanodesSp
for a, b, c being Element of FdSp st a,b congr c,c holds
a = b
proof end;

theorem :: PARSP_2:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FdSp being FanodesSp
for a, b being Element of FdSp st a,b congr b,a holds
a = b
proof end;

theorem Th58: :: PARSP_2:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th59: :: PARSP_2:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th60: :: PARSP_2:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th61: :: PARSP_2:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th62: :: PARSP_2:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PARSP_2:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PARSP_2:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PARSP_2:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th66: :: PARSP_2:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FdSp being FanodesSp
for a, b being Element of FdSp holds a,b congr a,b
proof end;

theorem Th67: :: PARSP_2:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PARSP_2:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: PARSP_2:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;