begin
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) )
Lm2:
for V being RealLinearSpace
for w, y being VECTOR of V holds (0 * w) + (0 * y) = 0. V
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)
:: 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 ) ) ) );
:: 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 )
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th5:
Lm5:
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
( w <> 0. V & y <> 0. V )
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
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 )
theorem Th12:
theorem Th13:
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 ) )
theorem Th14:
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 )
theorem Th15:
theorem Th16:
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
theorem Th17:
theorem Th18:
theorem Th19:
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:
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:
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 ) )
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
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
canceled;
theorem
canceled;
theorem Th22:
theorem Th23:
theorem
:: deftheorem ANALMETR:def 5 :
canceled;
:: 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
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)) #);
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem defines Af ANALMETR:def 8 :
for POS being non empty ParOrtStr holds Af POS = AffinStruct(# the carrier of POS, the CONGR of POS #);
theorem
canceled;
theorem Th30:
theorem Th31:
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 )
theorem Th32:
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 ) ) )
theorem Th33:
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
theorem Th34:
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
theorem Th35:
theorem Th36:
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
theorem Th37:
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 )
theorem Th38:
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
theorem Th39:
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
theorem Th40:
theorem
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
theorem Th42:
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 )
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;
verum
end;
definition
let IT be non
empty ParOrtStr ;
attr IT is
OrtAfSp-like means :
Def9:
(
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 ) ) ) );
theorem
canceled;
theorem
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;
verum
end;
definition
let IT be non
empty ParOrtStr ;
attr IT is
OrtAfPl-like means :
Def10:
(
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 ) ) ) );
theorem
canceled;
theorem
theorem
theorem Th48:
for
POS being non
empty ParOrtStr for
a,
b,
c,
d being
Element of
POS for
a9,
b9,
c9,
d9 being
Element of
(Af POS) st
a = a9 &
b = b9 &
c = c9 &
d = d9 holds
(
a,
b // c,
d iff
a9,
b9 // c9,
d9 )
theorem Th49:
theorem
theorem
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 ) ) ) ) ) )
:: 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:
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 )
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
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 ) );
:: 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) ) );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th55:
for
POS being
OrtAfSp for
a,
b,
c being
Element of
POS for
a9,
b9,
c9 being
Element of
(Af POS) st
a = a9 &
b = b9 &
c = c9 holds
(
LIN a,
b,
c iff
LIN a9,
b9,
c9 )
theorem Th56:
theorem
theorem Th58:
:: 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 ) );
:: 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 ) );
:: 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
canceled;
theorem
canceled;
theorem
canceled;
theorem Th62:
theorem Th63:
theorem Th64:
for
POS being
OrtAfSp for
M,
N being
Subset of
POS for
M9,
N9 being
Subset of
(Af POS) st
M = M9 &
N = N9 holds
(
M // N iff
M9 // N9 )
theorem
theorem
theorem
theorem
canceled;
theorem Th69:
theorem
canceled;
theorem Th71:
theorem
canceled;
theorem Th73:
theorem
canceled;
theorem
theorem Th76:
theorem
theorem Th78:
theorem
theorem Th80:
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 )
theorem Th81:
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 )
theorem
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
theorem Th83:
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 )
theorem Th84:
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
theorem Th85:
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
theorem
theorem
theorem Th88:
theorem Th89:
theorem
theorem Th91:
theorem