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

Lm1: for V being RealLinearSpace
for v1, w, y, v2 being VECTOR of V
for b1, b2, c1, c2 being Real st v1 = (b1 * w) + (b2 * y) & v2 = (c1 * w) + (c2 * y) holds
( v1 + v2 = ((b1 + c1) * w) + ((b2 + c2) * y) & v1 - v2 = ((b1 - c1) * w) + ((b2 - c2) * y) )
proof end;

Lm2: for V being RealLinearSpace
for w, y being VECTOR of V holds (0 * w) + (0 * y) = 0. V
proof end;

Lm3: for V being RealLinearSpace
for v, w, y being VECTOR of V
for b1, b2, a being Real st v = (b1 * w) + (b2 * y) holds
a * v = ((a * b1) * w) + ((a * b2) * y)
proof end;

definition
let V be RealLinearSpace;
let w, y be VECTOR of V;
pred Gen w,y means :Def1: :: ANALMETR:def 1
( ( for u being VECTOR of V ex a1, a2 being Real st u = (a1 * w) + (a2 * y) ) & ( for a1, a2 being Real st (a1 * w) + (a2 * y) = 0. V holds
( a1 = 0 & a2 = 0 ) ) );
end;

:: deftheorem Def1 defines Gen ANALMETR:def 1 :
for V being RealLinearSpace
for w, y being VECTOR of V holds
( Gen w,y iff ( ( for u being VECTOR of V ex a1, a2 being Real st u = (a1 * w) + (a2 * y) ) & ( for a1, a2 being Real st (a1 * w) + (a2 * y) = 0. V holds
( a1 = 0 & a2 = 0 ) ) ) );

definition
let V be RealLinearSpace;
let u, v, w, y be VECTOR of V;
pred u,v are_Ort_wrt w,y means :Def2: :: ANALMETR:def 2
ex a1, a2, b1, b2 being Real st
( u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) & (a1 * b1) + (a2 * b2) = 0 );
end;

:: deftheorem Def2 defines are_Ort_wrt ANALMETR:def 2 :
for V being RealLinearSpace
for u, v, w, y being VECTOR of V holds
( u,v are_Ort_wrt w,y iff ex a1, a2, b1, b2 being Real st
( u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) & (a1 * b1) + (a2 * b2) = 0 ) );

Lm4: for V being RealLinearSpace
for w, y being VECTOR of V
for a1, a2, b1, b2 being Real st Gen w,y & (a1 * w) + (a2 * y) = (b1 * w) + (b2 * y) holds
( a1 = b1 & a2 = b2 )
proof end;

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

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

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

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

theorem Th5: :: ANALMETR:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, v, w, y being VECTOR of V st Gen w,y holds
( u,v are_Ort_wrt w,y iff for a1, a2, b1, b2 being Real st u = (a1 * w) + (a2 * y) & v = (b1 * w) + (b2 * y) holds
(a1 * b1) + (a2 * b2) = 0 )
proof end;

Lm5: for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
( w <> 0. V & y <> 0. V )
proof end;

theorem :: ANALMETR:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y being VECTOR of V holds w,y are_Ort_wrt w,y
proof end;

theorem Th7: :: ANALMETR:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
ex V being RealLinearSpace ex w, y being VECTOR of V st Gen w,y
proof end;

theorem Th8: :: ANALMETR:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, v, w, y being VECTOR of V st u,v are_Ort_wrt w,y holds
v,u are_Ort_wrt w,y
proof end;

theorem Th9: :: ANALMETR:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for u, v being VECTOR of V holds
( u, 0. V are_Ort_wrt w,y & 0. V,v are_Ort_wrt w,y )
proof end;

theorem Th10: :: ANALMETR:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, v, w, y being VECTOR of V
for a, b being Real st u,v are_Ort_wrt w,y holds
a * u,b * v are_Ort_wrt w,y
proof end;

theorem Th11: :: ANALMETR:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, v, w, y being VECTOR of V
for a, b being Real st u,v are_Ort_wrt w,y holds
( a * u,v are_Ort_wrt w,y & u,b * v are_Ort_wrt w,y )
proof end;

theorem Th12: :: ANALMETR:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for u being VECTOR of V ex v being VECTOR of V st
( u,v are_Ort_wrt w,y & v <> 0. V )
proof end;

theorem Th13: :: ANALMETR:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y, v, u1, u2 being VECTOR of V st Gen w,y & v,u1 are_Ort_wrt w,y & v,u2 are_Ort_wrt w,y & v <> 0. V holds
ex a, b being Real st
( a * u1 = b * u2 & ( a <> 0 or b <> 0 ) )
proof end;

theorem Th14: :: ANALMETR:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y, u, v1, v2 being VECTOR of V st Gen w,y & u,v1 are_Ort_wrt w,y & u,v2 are_Ort_wrt w,y holds
( u,v1 + v2 are_Ort_wrt w,y & u,v1 - v2 are_Ort_wrt w,y )
proof end;

theorem Th15: :: ANALMETR:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y, u being VECTOR of V st Gen w,y & u,u are_Ort_wrt w,y holds
u = 0. V
proof end;

theorem Th16: :: ANALMETR:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y, u, u1, u2 being VECTOR of V st Gen w,y & u,u1 - u2 are_Ort_wrt w,y & u1,u2 - u are_Ort_wrt w,y holds
u2,u - u1 are_Ort_wrt w,y
proof end;

theorem Th17: :: ANALMETR:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y, u, v being VECTOR of V st Gen w,y & u <> 0. V holds
ex a being Real st v - (a * u),u are_Ort_wrt w,y
proof end;

theorem Th18: :: ANALMETR:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, v, u1, v1 being VECTOR of V holds
( ( u,v // u1,v1 or u,v // v1,u1 ) iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
proof end;

theorem Th19: :: ANALMETR:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, v, u1, v1 being VECTOR of V holds
( [[u,v],[u1,v1]] in lambda (DirPar V) iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
proof end;

definition
let V be RealLinearSpace;
let u, u1, v, v1, w, y be VECTOR of V;
pred u,u1,v,v1 are_Ort_wrt w,y means :Def3: :: ANALMETR:def 3
u1 - u,v1 - v are_Ort_wrt w,y;
end;

:: deftheorem Def3 defines are_Ort_wrt ANALMETR:def 3 :
for V being RealLinearSpace
for u, u1, v, v1, w, y being VECTOR of V holds
( u,u1,v,v1 are_Ort_wrt w,y iff u1 - u,v1 - v are_Ort_wrt w,y );

definition
let V be RealLinearSpace;
let w, y be VECTOR of V;
func Orthogonality V,w,y -> Relation of [:the carrier of V,the carrier of V:] means :Def4: :: ANALMETR:def 4
for x, z being set holds
( [x,z] in it iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) );
existence
ex b1 being Relation of [:the carrier of V,the carrier of V:] st
for x, z being set holds
( [x,z] in b1 iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) )
proof end;
uniqueness
for b1, b2 being Relation of [:the carrier of V,the carrier of V:] st ( for x, z being set holds
( [x,z] in b1 iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) ) & ( for x, z being set holds
( [x,z] in b2 iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Orthogonality ANALMETR:def 4 :
for V being RealLinearSpace
for w, y being VECTOR of V
for b4 being Relation of [:the carrier of V,the carrier of V:] holds
( b4 = Orthogonality V,w,y iff for x, z being set holds
( [x,z] in b4 iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_Ort_wrt w,y ) ) );

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

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

theorem Th22: :: ANALMETR:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace holds the carrier of (Lambda (OASpace V)) = the carrier of V
proof end;

theorem Th23: :: ANALMETR:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace holds the CONGR of (Lambda (OASpace V)) = lambda (DirPar V)
proof end;

theorem :: ANALMETR:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, v, u1, v1 being VECTOR of V
for p, q, p1, q1 being Element of (Lambda (OASpace V)) st p = u & q = v & p1 = u1 & q1 = v1 holds
( p,q // p1,q1 iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
proof end;

definition
attr c1 is strict;
struct ParOrtStr -> AffinStruct ;
aggr ParOrtStr(# carrier, CONGR, orthogonality #) -> ParOrtStr ;
sel orthogonality c1 -> Relation of [:the carrier of c1,the carrier of c1:];
end;

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

definition
let POS be non empty ParOrtStr ;
let a, b, c, d be Element of POS;
pred a,b // c,d means :Def5: :: ANALMETR:def 5
[[a,b],[c,d]] in the CONGR of POS;
pred a,b _|_ c,d means :Def6: :: ANALMETR:def 6
[[a,b],[c,d]] in the orthogonality of POS;
end;

:: deftheorem Def5 defines // ANALMETR:def 5 :
for POS being non empty ParOrtStr
for a, b, c, d being Element of POS holds
( a,b // c,d iff [[a,b],[c,d]] in the CONGR of POS );

:: deftheorem Def6 defines _|_ ANALMETR:def 6 :
for POS being non empty ParOrtStr
for a, b, c, d being Element of POS holds
( a,b _|_ c,d iff [[a,b],[c,d]] in the orthogonality of POS );

definition
let V be RealLinearSpace;
let w, y be VECTOR of V;
func AMSpace V,w,y -> strict ParOrtStr equals :: ANALMETR:def 7
ParOrtStr(# the carrier of V,(lambda (DirPar V)),(Orthogonality V,w,y) #);
correctness
coherence
ParOrtStr(# the carrier of V,(lambda (DirPar V)),(Orthogonality V,w,y) #) is strict ParOrtStr
;
;
end;

:: deftheorem defines AMSpace ANALMETR:def 7 :
for V being RealLinearSpace
for w, y being VECTOR of V holds AMSpace V,w,y = ParOrtStr(# the carrier of V,(lambda (DirPar V)),(Orthogonality V,w,y) #);

registration
let V be RealLinearSpace;
let w, y be VECTOR of V;
cluster AMSpace V,w,y -> non empty strict ;
coherence
not AMSpace V,w,y is empty
proof end;
end;

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

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

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

theorem :: ANALMETR:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y being VECTOR of V holds
( the carrier of (AMSpace V,w,y) = the carrier of V & the CONGR of (AMSpace V,w,y) = lambda (DirPar V) & the orthogonality of (AMSpace V,w,y) = Orthogonality V,w,y ) ;

definition
let POS be non empty ParOrtStr ;
func Af POS -> strict AffinStruct equals :: ANALMETR:def 8
AffinStruct(# the carrier of POS,the CONGR of POS #);
correctness
coherence
AffinStruct(# the carrier of POS,the CONGR of POS #) is strict AffinStruct
;
;
end;

:: deftheorem defines Af ANALMETR:def 8 :
for POS being non empty ParOrtStr holds Af POS = AffinStruct(# the carrier of POS,the CONGR of POS #);

registration
let POS be non empty ParOrtStr ;
cluster Af POS -> non empty strict ;
coherence
not Af POS is empty
proof end;
end;

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

theorem Th30: :: ANALMETR:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y being VECTOR of V holds Af (AMSpace V,w,y) = Lambda (OASpace V)
proof end;

theorem Th31: :: ANALMETR:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for u, u1, v, v1, w, y being VECTOR of V
for p, p1, q, q1 being Element of (AMSpace V,w,y) st p = u & p1 = u1 & q = v & q1 = v1 holds
( p,q _|_ p1,q1 iff u,v,u1,v1 are_Ort_wrt w,y )
proof end;

theorem Th32: :: ANALMETR:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y, u, v, u1, v1 being VECTOR of V
for p, q, p1, q1 being Element of (AMSpace V,w,y) st p = u & q = v & p1 = u1 & q1 = v1 holds
( p,q // p1,q1 iff ex a, b being Real st
( a * (v - u) = b * (v1 - u1) & ( a <> 0 or b <> 0 ) ) )
proof end;

theorem Th33: :: ANALMETR:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y being VECTOR of V
for p, q, p1, q1 being Element of (AMSpace V,w,y) st p,q _|_ p1,q1 holds
p1,q1 _|_ p,q
proof end;

theorem Th34: :: ANALMETR:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y being VECTOR of V
for p, q, p1, q1 being Element of (AMSpace V,w,y) st p,q _|_ p1,q1 holds
p,q _|_ q1,p1
proof end;

theorem Th35: :: ANALMETR:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for p, q, r being Element of (AMSpace V,w,y) holds p,q _|_ r,r
proof end;

theorem Th36: :: ANALMETR:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y being VECTOR of V
for p, p1, q, q1, r, r1 being Element of (AMSpace V,w,y) st p,p1 _|_ q,q1 & p,p1 // r,r1 & not p = p1 holds
q,q1 _|_ r,r1
proof end;

theorem Th37: :: ANALMETR:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for p, q, r being Element of (AMSpace V,w,y) ex r1 being Element of (AMSpace V,w,y) st
( p,q _|_ r,r1 & r <> r1 )
proof end;

theorem Th38: :: ANALMETR:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y being VECTOR of V
for p, p1, q, q1, r, r1 being Element of (AMSpace V,w,y) st Gen w,y & p,p1 _|_ q,q1 & p,p1 _|_ r,r1 & not p = p1 holds
q,q1 // r,r1
proof end;

theorem Th39: :: ANALMETR:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y being VECTOR of V
for p, q, r, r1, r2 being Element of (AMSpace V,w,y) st Gen w,y & p,q _|_ r,r1 & p,q _|_ r,r2 holds
p,q _|_ r1,r2
proof end;

theorem Th40: :: ANALMETR:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y being VECTOR of V
for p, q being Element of (AMSpace V,w,y) st Gen w,y & p,q _|_ p,q holds
p = q
proof end;

theorem :: ANALMETR:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y being VECTOR of V
for p, q, p1, p2 being Element of (AMSpace V,w,y) st Gen w,y & p,q _|_ p1,p2 & p1,q _|_ p2,p holds
p2,q _|_ p,p1
proof end;

theorem Th42: :: ANALMETR:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y being VECTOR of V
for p, p1 being Element of (AMSpace V,w,y) st Gen w,y & p <> p1 holds
for q being Element of (AMSpace V,w,y) ex q1 being Element of (AMSpace V,w,y) st
( p,p1 // p,q1 & p,p1 _|_ q1,q )
proof end;

consider V0 being RealLinearSpace such that
Lm6: ex w, y being VECTOR of V0 st Gen w,y by Th7;

consider w0, y0 being VECTOR of V0 such that
Lm7: Gen w0,y0 by Lm6;

Lm8: now
set X = AffinStruct(# the carrier of (AMSpace V0,w0,y0),the CONGR of (AMSpace V0,w0,y0) #);
AffinStruct(# the carrier of (AMSpace V0,w0,y0),the CONGR of (AMSpace V0,w0,y0) #) = Af (AMSpace V0,w0,y0) ;
then A1: AffinStruct(# the carrier of (AMSpace V0,w0,y0),the CONGR of (AMSpace V0,w0,y0) #) = Lambda (OASpace V0) by Th30;
for a, b being Real st (a * w0) + (b * y0) = 0. V0 holds
( a = 0 & b = 0 ) by Def1, Lm7;
then OASpace V0 is OAffinSpace by ANALOAF:38;
hence ( AffinStruct(# the carrier of (AMSpace V0,w0,y0),the CONGR of (AMSpace V0,w0,y0) #) is AffinSpace & ( for a, b, c, d, p, q, r, s being Element of (AMSpace V0,w0,y0) holds
( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ p,s implies a,b _|_ q,s ) ) ) & ( for a, b, c being Element of (AMSpace V0,w0,y0) st a <> b holds
ex x being Element of (AMSpace V0,w0,y0) st
( a,b // a,x & a,b _|_ x,c ) ) & ( for a, b, c being Element of (AMSpace V0,w0,y0) ex x being Element of (AMSpace V0,w0,y0) st
( a,b _|_ c,x & c <> x ) ) ) by A1, Lm7, Th33, Th34, Th35, Th36, Th37, Th39, Th40, Th42, DIRAF:48; :: thesis: verum
end;

definition
let IT be non empty ParOrtStr ;
attr IT is OrtAfSp-like means :Def9: :: ANALMETR:def 9
( AffinStruct(# the carrier of IT,the CONGR of IT #) is AffinSpace & ( for a, b, c, d, p, q, r, s being Element of IT holds
( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ p,s implies a,b _|_ q,s ) ) ) & ( for a, b, c being Element of IT st a <> b holds
ex x being Element of IT st
( a,b // a,x & a,b _|_ x,c ) ) & ( for a, b, c being Element of IT ex x being Element of IT st
( a,b _|_ c,x & c <> x ) ) );
end;

:: deftheorem Def9 defines OrtAfSp-like ANALMETR:def 9 :
for IT being non empty ParOrtStr holds
( IT is OrtAfSp-like iff ( AffinStruct(# the carrier of IT,the CONGR of IT #) is AffinSpace & ( for a, b, c, d, p, q, r, s being Element of IT holds
( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ p,s implies a,b _|_ q,s ) ) ) & ( for a, b, c being Element of IT st a <> b holds
ex x being Element of IT st
( a,b // a,x & a,b _|_ x,c ) ) & ( for a, b, c being Element of IT ex x being Element of IT st
( a,b _|_ c,x & c <> x ) ) ) );

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

definition
mode OrtAfSp is non empty OrtAfSp-like ParOrtStr ;
end;

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

theorem :: ANALMETR:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
AMSpace V,w,y is OrtAfSp
proof end;

consider V0 being RealLinearSpace such that
Lm9: ex w, y being VECTOR of V0 st Gen w,y by Th7;

consider w0, y0 being VECTOR of V0 such that
Lm10: Gen w0,y0 by Lm9;

Lm11: now
set X = AffinStruct(# the carrier of (AMSpace V0,w0,y0),the CONGR of (AMSpace V0,w0,y0) #);
AffinStruct(# the carrier of (AMSpace V0,w0,y0),the CONGR of (AMSpace V0,w0,y0) #) = Af (AMSpace V0,w0,y0) ;
then A1: AffinStruct(# the carrier of (AMSpace V0,w0,y0),the CONGR of (AMSpace V0,w0,y0) #) = Lambda (OASpace V0) by Th30;
( ( for a, b being Real st (a * w0) + (b * y0) = 0. V0 holds
( a = 0 & b = 0 ) ) & ( for w1 being VECTOR of V0 ex a, b being Real st w1 = (a * w0) + (b * y0) ) ) by Def1, Lm10;
then OASpace V0 is OAffinPlane by ANALOAF:51;
hence ( AffinStruct(# the carrier of (AMSpace V0,w0,y0),the CONGR of (AMSpace V0,w0,y0) #) is AffinPlane & ( for a, b, c, d, p, q, r, s being Element of (AMSpace V0,w0,y0) holds
( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) ) ) & ( for a, b, c being Element of (AMSpace V0,w0,y0) ex x being Element of (AMSpace V0,w0,y0) st
( a,b _|_ c,x & c <> x ) ) ) by A1, Lm10, Th33, Th34, Th35, Th36, Th37, Th38, Th40, DIRAF:53; :: thesis: verum
end;

definition
let IT be non empty ParOrtStr ;
attr IT is OrtAfPl-like means :Def10: :: ANALMETR:def 10
( AffinStruct(# the carrier of IT,the CONGR of IT #) is AffinPlane & ( for a, b, c, d, p, q, r, s being Element of IT holds
( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) ) ) & ( for a, b, c being Element of IT ex x being Element of IT st
( a,b _|_ c,x & c <> x ) ) );
end;

:: deftheorem Def10 defines OrtAfPl-like ANALMETR:def 10 :
for IT being non empty ParOrtStr holds
( IT is OrtAfPl-like iff ( AffinStruct(# the carrier of IT,the CONGR of IT #) is AffinPlane & ( for a, b, c, d, p, q, r, s being Element of IT holds
( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) ) ) & ( for a, b, c being Element of IT ex x being Element of IT st
( a,b _|_ c,x & c <> x ) ) ) );

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

definition
mode OrtAfPl is non empty OrtAfPl-like ParOrtStr ;
end;

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

theorem :: ANALMETR:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
AMSpace V,w,y is OrtAfPl
proof end;

theorem :: ANALMETR:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being non empty ParOrtStr
for x being set holds
( x is Element of POS iff x is Element of (Af POS) ) ;

theorem Th48: :: ANALMETR:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being non empty ParOrtStr
for a, b, c, d being Element of POS
for a', b', c', d' being Element of (Af POS) st a = a' & b = b' & c = c' & d = d' holds
( a,b // c,d iff a',b' // c',d' )
proof end;

Lm12: for POS being OrtAfSp holds Af POS is AffinSpace
by Def9;

registration
let POS be OrtAfSp;
cluster Af POS -> non empty non trivial strict AffinSpace-like ;
correctness
coherence
( Af POS is AffinSpace-like & not Af POS is trivial )
;
by Lm12;
end;

Lm13: for POS being OrtAfPl holds Af POS is AffinPlane
by Def10;

registration
let POS be OrtAfPl;
cluster Af POS -> non empty non trivial strict AffinSpace-like 2-dimensional ;
correctness
coherence
( Af POS is 2-dimensional & Af POS is AffinSpace-like & not Af POS is trivial )
;
by Lm13;
end;

theorem Th49: :: ANALMETR:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfPl holds POS is OrtAfSp
proof end;

registration
cluster non empty OrtAfPl-like -> non empty OrtAfSp-like ParOrtStr ;
coherence
for b1 being non empty ParOrtStr st b1 is OrtAfPl-like holds
b1 is OrtAfSp-like
by Th49;
end;

theorem :: ANALMETR:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp st Af POS is AffinPlane holds
POS is OrtAfPl
proof end;

theorem :: ANALMETR:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being non empty ParOrtStr holds
( POS is OrtAfPl-like iff ( ex a, b being Element of POS st a <> b & ( for a, b, c, d, p, q, r, s being Element of POS 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 POS st
( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) ) ) ) )
proof end;

definition
let POS be non empty ParOrtStr ;
let a, b, c be Element of POS;
pred LIN a,b,c means :Def11: :: ANALMETR:def 11
a,b // a,c;
end;

:: deftheorem Def11 defines LIN ANALMETR:def 11 :
for POS being non empty ParOrtStr
for a, b, c being Element of POS holds
( LIN a,b,c iff a,b // a,c );

definition
let POS be non empty ParOrtStr ;
let a, b be Element of POS;
func Line a,b -> Subset of POS means :Def12: :: ANALMETR:def 12
for x being Element of POS holds
( x in it iff LIN a,b,x );
existence
ex b1 being Subset of POS st
for x being Element of POS holds
( x in b1 iff LIN a,b,x )
proof end;
uniqueness
for b1, b2 being Subset of POS st ( for x being Element of POS holds
( x in b1 iff LIN a,b,x ) ) & ( for x being Element of POS holds
( x in b2 iff LIN a,b,x ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines Line ANALMETR:def 12 :
for POS being non empty ParOrtStr
for a, b being Element of POS
for b4 being Subset of POS holds
( b4 = Line a,b iff for x being Element of POS holds
( x in b4 iff LIN a,b,x ) );

definition
let POS be non empty ParOrtStr ;
let A be Subset of POS;
attr A is being_line means :Def13: :: ANALMETR:def 13
ex a, b being Element of POS st
( a <> b & A = Line a,b );
end;

:: deftheorem Def13 defines being_line ANALMETR:def 13 :
for POS being non empty ParOrtStr
for A being Subset of POS holds
( A is being_line iff ex a, b being Element of POS st
( a <> b & A = Line a,b ) );

notation
let POS be non empty ParOrtStr ;
let A be Subset of POS;
synonym A is_line for being_line A;
end;

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

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

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

theorem Th55: :: ANALMETR:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for a, b, c being Element of POS
for a', b', c' being Element of (Af POS) st a = a' & b = b' & c = c' holds
( LIN a,b,c iff LIN a',b',c' )
proof end;

theorem Th56: :: ANALMETR:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for a, b being Element of POS
for a', b' being Element of (Af POS) st a = a' & b = b' holds
Line a,b = Line a',b'
proof end;

theorem :: ANALMETR:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being non empty ParOrtStr
for X being set holds
( X is Subset of POS iff X is Subset of (Af POS) ) ;

theorem Th58: :: ANALMETR:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for X being Subset of POS
for Y being Subset of (Af POS) st X = Y holds
( X is_line iff Y is_line )
proof end;

definition
let POS be non empty ParOrtStr ;
let a, b be Element of POS;
let K be Subset of POS;
pred a,b _|_ K means :Def14: :: ANALMETR:def 14
ex p, q being Element of POS st
( p <> q & K = Line p,q & a,b _|_ p,q );
end;

:: deftheorem Def14 defines _|_ ANALMETR:def 14 :
for POS being non empty ParOrtStr
for a, b being Element of POS
for K being Subset of POS holds
( a,b _|_ K iff ex p, q being Element of POS st
( p <> q & K = Line p,q & a,b _|_ p,q ) );

definition
let POS be non empty ParOrtStr ;
let K, M be Subset of POS;
pred K _|_ M means :Def15: :: ANALMETR:def 15
ex p, q being Element of POS st
( p <> q & K = Line p,q & p,q _|_ M );
end;

:: deftheorem Def15 defines _|_ ANALMETR:def 15 :
for POS being non empty ParOrtStr
for K, M being Subset of POS holds
( K _|_ M iff ex p, q being Element of POS st
( p <> q & K = Line p,q & p,q _|_ M ) );

definition
let POS be non empty ParOrtStr ;
let K, M be Subset of POS;
pred K // M means :Def16: :: ANALMETR:def 16
ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line a,b & M = Line c,d & a,b // c,d );
end;

:: deftheorem Def16 defines // ANALMETR:def 16 :
for POS being non empty ParOrtStr
for K, M being Subset of POS holds
( K // M iff ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line a,b & M = Line c,d & a,b // c,d ) );

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

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

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

theorem Th62: :: ANALMETR:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being non empty ParOrtStr
for a, b being Element of POS
for K, M being Subset of POS holds
( ( a,b _|_ K implies K is_line ) & ( K _|_ M implies ( K is_line & M is_line ) ) )
proof end;

theorem Th63: :: ANALMETR:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being non empty ParOrtStr
for K, M being Subset of POS holds
( K _|_ M iff ex a, b, c, d being Element of POS st
( a <> b & c <> d & K = Line a,b & M = Line c,d & a,b _|_ c,d ) )
proof end;

theorem Th64: :: ANALMETR:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for M, N being Subset of POS
for M', N' being Subset of (Af POS) st M = M' & N = N' holds
( M // N iff M' // N' )
proof end;

theorem :: ANALMETR:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for K being Subset of POS
for a being Element of POS st K is_line holds
a,a _|_ K
proof end;

theorem :: ANALMETR:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for K being Subset of POS
for a, b, c, d being Element of POS st a,b _|_ K & ( a,b // c,d or c,d // a,b ) & a <> b holds
c,d _|_ K
proof end;

theorem :: ANALMETR:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for K being Subset of POS
for a, b being Element of POS st a,b _|_ K holds
b,a _|_ K
proof end;

theorem Th68: :: ANALMETR:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for K, M being Subset of POS st K // M holds
M // K
proof end;

theorem Th69: :: ANALMETR:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for K, M being Subset of POS
for r, s being Element of POS st r,s _|_ K & ( K // M or M // K ) holds
r,s _|_ M
proof end;

theorem Th70: :: ANALMETR:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for K, M being Subset of POS st K _|_ M holds
M _|_ K
proof end;

definition
let POS be OrtAfSp;
let K, M be Subset of POS;
:: original: //
redefine pred K // M;
symmetry
for K, M being Subset of POS st K // M holds
M // K
by Th68;
:: original: _|_
redefine pred K _|_ M;
symmetry
for K, M being Subset of POS st K _|_ M holds
M _|_ K
by Th70;
end;

theorem Th71: :: ANALMETR:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for K being Subset of POS
for a, b being Element of POS st a in K & b in K & a,b _|_ K holds
a = b
proof end;

theorem Th72: :: ANALMETR:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for K being Subset of POS holds not K _|_ K
proof end;

theorem Th73: :: ANALMETR:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for K, M, N being Subset of POS st ( K _|_ M or M _|_ K ) & ( K // N or N // K ) holds
( M _|_ N & N _|_ M )
proof end;

theorem Th74: :: ANALMETR:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for K, N being Subset of POS st K // N holds
not K _|_ N
proof end;

theorem :: ANALMETR:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for K being Subset of POS
for a, b, c, d being Element of POS st a in K & b in K & c,d _|_ K holds
( c,d _|_ a,b & a,b _|_ c,d )
proof end;

theorem Th76: :: ANALMETR:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for K being Subset of POS
for a, b being Element of POS st a in K & b in K & a <> b & K is_line holds
K = Line a,b
proof end;

theorem :: ANALMETR:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for K being Subset of POS
for a, b, c, d being Element of POS st a in K & b in K & a <> b & K is_line & ( a,b _|_ c,d or c,d _|_ a,b ) holds
c,d _|_ K
proof end;

theorem Th78: :: ANALMETR:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for M, N being Subset of POS
for a, b, c, d being Element of POS st a in M & b in M & c in N & d in N & M _|_ N holds
a,b _|_ c,d
proof end;

theorem :: ANALMETR:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for M, N, K, A being Subset of POS
for p, a, b being Element of POS st p in M & p in N & a in M & b in N & a <> b & a in K & b in K & A _|_ M & A _|_ N & K is_line holds
A _|_ K
proof end;

theorem Th80: :: ANALMETR:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for b, c, a being Element of POS holds
( b,c _|_ a,a & a,a _|_ b,c & b,c // a,a & a,a // b,c )
proof end;

theorem Th81: :: ANALMETR:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for a, b, c, d being Element of POS st a,b // c,d holds
( a,b // d,c & b,a // c,d & b,a // d,c & c,d // a,b & c,d // b,a & d,c // a,b & d,c // b,a )
proof end;

theorem :: ANALMETR:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for p, q, a, b, c, d being Element of POS st p <> q & ( ( p,q // a,b & p,q // c,d ) or ( p,q // a,b & c,d // p,q ) or ( a,b // p,q & c,d // p,q ) or ( a,b // p,q & p,q // c,d ) ) holds
a,b // c,d
proof end;

theorem Th83: :: ANALMETR:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for a, b, c, d being Element of POS st a,b _|_ c,d holds
( a,b _|_ d,c & b,a _|_ c,d & b,a _|_ d,c & c,d _|_ a,b & c,d _|_ b,a & d,c _|_ a,b & d,c _|_ b,a )
proof end;

theorem Th84: :: ANALMETR:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfSp
for p, q, a, b, c, d being Element of POS st p <> q & ( ( p,q // a,b & p,q _|_ c,d ) or ( p,q // c,d & p,q _|_ a,b ) or ( p,q // a,b & c,d _|_ p,q ) or ( p,q // c,d & a,b _|_ p,q ) or ( a,b // p,q & c,d _|_ p,q ) or ( c,d // p,q & a,b _|_ p,q ) or ( a,b // p,q & p,q _|_ c,d ) or ( c,d // p,q & p,q _|_ a,b ) ) holds
a,b _|_ c,d
proof end;

theorem Th85: :: ANALMETR:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfPl
for p, q, a, b, c, d being Element of POS st p <> q & ( ( p,q _|_ a,b & p,q _|_ c,d ) or ( p,q _|_ a,b & c,d _|_ p,q ) or ( a,b _|_ p,q & c,d _|_ p,q ) or ( a,b _|_ p,q & p,q _|_ c,d ) ) holds
a,b // c,d
proof end;

theorem :: ANALMETR:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfPl
for M, N being Subset of POS
for a, b, c, d being Element of POS st a in M & b in M & a <> b & M is_line & c in N & d in N & c <> d & N is_line & a,b // c,d holds
M // N
proof end;

theorem :: ANALMETR:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfPl
for K, M, N being Subset of POS st ( K _|_ M or M _|_ K ) & ( K _|_ N or N _|_ K ) holds
( M // N & N // M )
proof end;

theorem Th88: :: ANALMETR:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfPl
for M, N being Subset of POS st M _|_ N holds
ex p being Element of POS st
( p in M & p in N )
proof end;

theorem Th89: :: ANALMETR:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfPl
for a, b, c, d being Element of POS st a,b _|_ c,d holds
ex p being Element of POS st
( LIN a,b,p & LIN c,d,p )
proof end;

theorem :: ANALMETR:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfPl
for K being Subset of POS
for a, b being Element of POS st a,b _|_ K holds
ex p being Element of POS st
( LIN a,b,p & p in K )
proof end;

theorem Th91: :: ANALMETR:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfPl
for a, p, q being Element of POS ex x being Element of POS st
( a,x _|_ p,q & LIN p,q,x )
proof end;

theorem :: ANALMETR:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for POS being OrtAfPl
for K being Subset of POS
for a being Element of POS st K is_line holds
ex x being Element of POS st
( a,x _|_ K & x in K )
proof end;