:: One-Dimensional Congruence of Segments, Basic Facts and Midpoint Relation
:: by Barbara Konstanta, Urszula Kowieska, Grzegorz Lewandowski and
::
:: Received October 4, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users

registration

let A be non empty set ;
let C be Relation of [:A,A:];

cluster AffinStruct(# A,C #) -> non empty ;

coherence
not AffinStruct(# A,C #) is empty ;

end;

Lm1: for AFV being WeakAffVect
for a, b, c being Element of AFV st a,b '||' b,c & a <> c holds
a,b // b,c

proof end;

Lm2: for AFV being WeakAffVect
for a, b being Element of AFV holds
( a,b // b,a iff ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) )

proof end;

Lm3: for AFV being WeakAffVect
for a, b, c, d being Element of AFV st a,b '||' c,d holds
b,a '||' c,d

proof end;

Lm4: for AFV being WeakAffVect
for a, b being Element of AFV holds a,b '||' b,a

proof end;

Lm5: for AFV being WeakAffVect
for a, b, p being Element of AFV st a,b '||' p,p holds
a = b

proof end;

Lm6: for AFV being WeakAffVect
for a, b, c, d, p, q being Element of AFV st a,b '||' p,q & c,d '||' p,q holds
a,b '||' c,d

proof end;

Lm7: for AFV being WeakAffVect
for a, c being Element of AFV ex b being Element of AFV st a,b '||' b,c

proof end;

Lm8: for AFV being WeakAffVect
for a, a9, b, b9, p being Element of AFV st a <> a9 & b <> b9 & p,a '||' p,a9 & p,b '||' p,b9 holds
a,b '||' a9,b9

proof end;

Lm9: for AFV being WeakAffVect
for a, b being Element of AFV holds
( a = b or ex c being Element of AFV st
( ( a <> c & a,b '||' b,c ) or ex p, p9 being Element of AFV st
( p <> p9 & a,b '||' p,p9 & a,p '||' p,b & a,p9 '||' p9,b ) ) )

proof end;

Lm10: for AFV being WeakAffVect
for a, b, b9, p, p9, c being Element of AFV st a,b '||' b,c & b,b9 '||' p,p9 & b,p '||' p,b9 & b,p9 '||' p9,b9 holds
a,b9 '||' b9,c

proof end;

Lm11: for AFV being WeakAffVect
for a, b, b9, c being Element of AFV st a <> c & b <> b9 & a,b '||' b,c & a,b9 '||' b9,c holds
ex p, p9 being Element of AFV st
( p <> p9 & b,b9 '||' p,p9 & b,p '||' p,b9 & b,p9 '||' p9,b9 )

proof end;

Lm12: for AFV being WeakAffVect
for a, b, c, p, p9, q, q9 being Element of AFV st a,b '||' p,p9 & a,c '||' q,q9 & a,p '||' p,b & a,q '||' q,c & a,p9 '||' p9,b & a,q9 '||' q9,c holds
ex r, r9 being Element of AFV st
( b,c '||' r,r9 & b,r '||' r,c & b,r9 '||' r9,c )

proof end;

set AFV0 = the WeakAffVect;

set X = the carrier of the WeakAffVect;

set XX = [: the carrier of the WeakAffVect, the carrier of the WeakAffVect:];

defpred S₁[ object , object ] means ex a, b, c, d being Element of the carrier of the WeakAffVect st
( $1 = [a,b] & $2 = [c,d] & a,b '||' c,d );

consider P being Relation of [: the carrier of the WeakAffVect, the carrier of the WeakAffVect:],[: the carrier of the WeakAffVect, the carrier of the WeakAffVect:] such that
Lm13: for x, y being object holds
( [x,y] in P iff ( x in [: the carrier of the WeakAffVect, the carrier of the WeakAffVect:] & y in [: the carrier of the WeakAffVect, the carrier of the WeakAffVect:] & S₁[x,y] ) ) from RELSET_1:sch 1();

Lm14: for a, b, c, d being Element of the carrier of the WeakAffVect holds
( [[a,b],[c,d]] in P iff a,b '||' c,d )

proof end;

set WAS = AffinStruct(# the carrier of the WeakAffVect,P #);

Lm15: for a, b, c, d being Element of the WeakAffVect
for a9, b9, c9, d9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a = a9 & b = b9 & c = c9 & d = d9 holds
( a,b '||' c,d iff a9,b9 // c9,d9 )

proof end;

Lm16: now :: thesis: ( ex a9, b9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a9 <> b9 & ( for a9, b9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) holds a9,b9 // b9,a9 ) & ( for a9, b9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a9,b9 // a9,a9 holds
a9 = b9 ) & ( for a, b, c, d, p, q being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,q & c,d // p,q holds
a,b // c,d ) & ( for a, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) ex b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c ) & ( for a, a9, b, b9, p being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> a9 & b <> b9 & p,a // p,a9 & p,b // p,b9 holds
a,b // a9,b9 ) & ( for a, b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) holds
( a = b or ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( ( a <> c & a,b // b,c ) or ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) ) ) & ( for a, b, b9, p, p9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 holds
a,b9 // b9,c ) & ( for a, b, b9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c holds
ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) ) & ( for a, b, c, p, p9, q, q9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds
ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) ) )

thus ex a9, b9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a9 <> b9 by STRUCT_0:def 10; :: thesis: ( ( for a9, b9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) holds a9,b9 // b9,a9 ) & ( for a9, b9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a9,b9 // a9,a9 holds
a9 = b9 ) & ( for a, b, c, d, p, q being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,q & c,d // p,q holds
a,b // c,d ) & ( for a, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) ex b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c ) & ( for a, a9, b, b9, p being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> a9 & b <> b9 & p,a // p,a9 & p,b // p,b9 holds
a,b // a9,b9 ) & ( for a, b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) holds
( a = b or ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( ( a <> c & a,b // b,c ) or ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) ) ) & ( for a, b, b9, p, p9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 holds
a,b9 // b9,c ) & ( for a, b, b9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c holds
ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) ) & ( for a, b, c, p, p9, q, q9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds
ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) ) )
thus for a9, b9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) holds a9,b9 // b9,a9 :: thesis: ( ( for a9, b9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a9,b9 // a9,a9 holds
a9 = b9 ) & ( for a, b, c, d, p, q being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,q & c,d // p,q holds
a,b // c,d ) & ( for a, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) ex b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c ) & ( for a, a9, b, b9, p being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> a9 & b <> b9 & p,a // p,a9 & p,b // p,b9 holds
a,b // a9,b9 ) & ( for a, b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) holds
( a = b or ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( ( a <> c & a,b // b,c ) or ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) ) ) & ( for a, b, b9, p, p9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 holds
a,b9 // b9,c ) & ( for a, b, b9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c holds
ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) ) & ( for a, b, c, p, p9, q, q9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds
ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) ) )

proof

let a9, b9 be Element of AffinStruct(# the carrier of the WeakAffVect,P #); :: thesis: a9,b9 // b9,a9
reconsider a = a9, b = b9 as Element of the WeakAffVect ;
a,b '||' b,a by Lm4;
hence a9,b9 // b9,a9 by Lm15; :: thesis: verum

end;

thus for a9, b9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a9,b9 // a9,a9 holds
a9 = b9 :: thesis: ( ( for a, b, c, d, p, q being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,q & c,d // p,q holds
a,b // c,d ) & ( for a, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) ex b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c ) & ( for a, a9, b, b9, p being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> a9 & b <> b9 & p,a // p,a9 & p,b // p,b9 holds
a,b // a9,b9 ) & ( for a, b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) holds
( a = b or ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( ( a <> c & a,b // b,c ) or ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) ) ) & ( for a, b, b9, p, p9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 holds
a,b9 // b9,c ) & ( for a, b, b9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c holds
ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) ) & ( for a, b, c, p, p9, q, q9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds
ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) ) )

proof

let a9, b9 be Element of AffinStruct(# the carrier of the WeakAffVect,P #); :: thesis: ( a9,b9 // a9,a9 implies a9 = b9 )
assume A1: a9,b9 // a9,a9 ; :: thesis: a9 = b9
reconsider a = a9, b = b9 as Element of the WeakAffVect ;
a,b '||' a,a by A1, Lm15;
hence a9 = b9 by Lm5; :: thesis: verum

end;

thus for a, b, c, d, p, q being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,q & c,d // p,q holds
a,b // c,d :: thesis: ( ( for a, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) ex b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c ) & ( for a, a9, b, b9, p being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> a9 & b <> b9 & p,a // p,a9 & p,b // p,b9 holds
a,b // a9,b9 ) & ( for a, b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) holds
( a = b or ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( ( a <> c & a,b // b,c ) or ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) ) ) & ( for a, b, b9, p, p9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 holds
a,b9 // b9,c ) & ( for a, b, b9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c holds
ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) ) & ( for a, b, c, p, p9, q, q9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds
ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) ) )

proof

let a, b, c, d, p, q be Element of AffinStruct(# the carrier of the WeakAffVect,P #); :: thesis: ( a,b // p,q & c,d // p,q implies a,b // c,d )
assume A2: ( a,b // p,q & c,d // p,q ) ; :: thesis: a,b // c,d
reconsider a1 = a, b1 = b, c1 = c, d1 = d, p1 = p, q1 = q as Element of the WeakAffVect ;
( a1,b1 '||' p1,q1 & c1,d1 '||' p1,q1 ) by A2, Lm15;
then a1,b1 '||' c1,d1 by Lm6;
hence a,b // c,d by Lm15; :: thesis: verum

end;

thus for a, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) ex b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c :: thesis: ( ( for a, a9, b, b9, p being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> a9 & b <> b9 & p,a // p,a9 & p,b // p,b9 holds
a,b // a9,b9 ) & ( for a, b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) holds
( a = b or ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( ( a <> c & a,b // b,c ) or ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) ) ) & ( for a, b, b9, p, p9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 holds
a,b9 // b9,c ) & ( for a, b, b9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c holds
ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) ) & ( for a, b, c, p, p9, q, q9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds
ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) ) )

proof

let a, c be Element of AffinStruct(# the carrier of the WeakAffVect,P #); :: thesis: ex b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c
reconsider a1 = a, c1 = c as Element of the WeakAffVect ;
consider b1 being Element of the WeakAffVect such that
A3: a1,b1 '||' b1,c1 by Lm7;
reconsider b = b1 as Element of AffinStruct(# the carrier of the WeakAffVect,P #) ;
a,b // b,c by A3, Lm15;
hence ex b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c ; :: thesis: verum

end;

thus for a, a9, b, b9, p being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> a9 & b <> b9 & p,a // p,a9 & p,b // p,b9 holds
a,b // a9,b9 :: thesis: ( ( for a, b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) holds
( a = b or ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( ( a <> c & a,b // b,c ) or ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) ) ) & ( for a, b, b9, p, p9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 holds
a,b9 // b9,c ) & ( for a, b, b9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c holds
ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) ) & ( for a, b, c, p, p9, q, q9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds
ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) ) )

proof

let a, a9, b, b9, p be Element of AffinStruct(# the carrier of the WeakAffVect,P #); :: thesis: ( a <> a9 & b <> b9 & p,a // p,a9 & p,b // p,b9 implies a,b // a9,b9 )
assume that
A4: ( a <> a9 & b <> b9 ) and
A5: ( p,a // p,a9 & p,b // p,b9 ) ; :: thesis: a,b // a9,b9
reconsider a1 = a, a19 = a9, b1 = b, b19 = b9, p1 = p as Element of the WeakAffVect ;
( p1,a1 '||' p1,a19 & p1,b1 '||' p1,b19 ) by A5, Lm15;
then a1,b1 '||' a19,b19 by A4, Lm8;
hence a,b // a9,b9 by Lm15; :: thesis: verum

end;

thus for a, b being Element of AffinStruct(# the carrier of the WeakAffVect,P #) holds
( a = b or ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( ( a <> c & a,b // b,c ) or ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) ) :: thesis: ( ( for a, b, b9, p, p9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 holds
a,b9 // b9,c ) & ( for a, b, b9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c holds
ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) ) & ( for a, b, c, p, p9, q, q9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds
ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) ) )

proof

let a, b be Element of AffinStruct(# the carrier of the WeakAffVect,P #); :: thesis: ( a = b or ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( ( a <> c & a,b // b,c ) or ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) )
assume A6: not a = b ; :: thesis: ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( ( a <> c & a,b // b,c ) or ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) )
reconsider a1 = a, b1 = b as Element of the WeakAffVect ;

A7: now :: thesis: ( ex p1, p19 being Element of the WeakAffVect st
( p1 <> p19 & a1,b1 '||' p1,p19 & a1,p1 '||' p1,b1 & a1,p19 '||' p19,b1 ) implies ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) )

given p1, p19 being Element of the WeakAffVect such that A8: p1 <> p19 and
A9: ( a1,b1 '||' p1,p19 & a1,p1 '||' p1,b1 ) and
A10: a1,p19 '||' p19,b1 ; :: thesis: ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b )
reconsider p = p1, p9 = p19 as Element of AffinStruct(# the carrier of the WeakAffVect,P #) ;
A11: a,p9 // p9,b by A10, Lm15;
( a,b // p,p9 & a,p // p,b ) by A9, Lm15;
hence ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) by A8, A11; :: thesis: verum

end;

now :: thesis: ( ex c1 being Element of the WeakAffVect st
( a1 <> c1 & a1,b1 '||' b1,c1 ) implies ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( a <> c & a,b // b,c ) )

given c1 being Element of the WeakAffVect such that A12: a1 <> c1 and
A13: a1,b1 '||' b1,c1 ; :: thesis: ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( a <> c & a,b // b,c )
reconsider c = c1 as Element of AffinStruct(# the carrier of the WeakAffVect,P #) ;
a,b // b,c by A13, Lm15;
hence ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( a <> c & a,b // b,c ) by A12; :: thesis: verum

end;

hence ex c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( ( a <> c & a,b // b,c ) or ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) by A6, A7, Lm9; :: thesis: verum

end;

thus for a, b, b9, p, p9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 holds
a,b9 // b9,c :: thesis: ( ( for a, b, b9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c holds
ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) ) & ( for a, b, c, p, p9, q, q9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds
ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) ) )

proof

let a, b, b9, p, p9, c be Element of AffinStruct(# the carrier of the WeakAffVect,P #); :: thesis: ( a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 implies a,b9 // b9,c )
assume that
A14: ( a,b // b,c & b,b9 // p,p9 ) and
A15: ( b,p // p,b9 & b,p9 // p9,b9 ) ; :: thesis: a,b9 // b9,c
reconsider a1 = a, b1 = b, b19 = b9, p1 = p, p19 = p9, c1 = c as Element of the WeakAffVect ;
A16: ( b1,p1 '||' p1,b19 & b1,p19 '||' p19,b19 ) by A15, Lm15;
( a1,b1 '||' b1,c1 & b1,b19 '||' p1,p19 ) by A14, Lm15;
then a1,b19 '||' b19,c1 by A16, Lm10;
hence a,b9 // b9,c by Lm15; :: thesis: verum

end;

thus for a, b, b9, c being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c holds
ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) :: thesis: for a, b, c, p, p9, q, q9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds
ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( b,c // r,r9 & b,r // r,c & b,r9 // r9,c )

proof

let a, b, b9, c be Element of AffinStruct(# the carrier of the WeakAffVect,P #); :: thesis: ( a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c implies ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) )
assume that
A17: ( a <> c & b <> b9 ) and
A18: ( a,b // b,c & a,b9 // b9,c ) ; :: thesis: ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 )
reconsider a1 = a, b1 = b, b19 = b9, c1 = c as Element of the WeakAffVect ;
( a1,b1 '||' b1,c1 & a1,b19 '||' b19,c1 ) by A18, Lm15;
then consider p1, p19 being Element of the WeakAffVect such that
A19: p1 <> p19 and
A20: ( b1,b19 '||' p1,p19 & b1,p1 '||' p1,b19 ) and
A21: b1,p19 '||' p19,b19 by A17, Lm11;
reconsider p = p1, p9 = p19 as Element of AffinStruct(# the carrier of the WeakAffVect,P #) ;
A22: b,p9 // p9,b9 by A21, Lm15;
( b,b9 // p,p9 & b,p // p,b9 ) by A20, Lm15;
hence ex p, p9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) by A19, A22; :: thesis: verum

end;

thus for a, b, c, p, p9, q, q9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds
ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) :: thesis: verum

proof

let a, b, c, p, p9, q, q9 be Element of AffinStruct(# the carrier of the WeakAffVect,P #); :: thesis: ( a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c implies ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) )
assume that
A23: ( a,b // p,p9 & a,c // q,q9 ) and
A24: ( a,p // p,b & a,q // q,c ) and
A25: ( a,p9 // p9,b & a,q9 // q9,c ) ; :: thesis: ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( b,c // r,r9 & b,r // r,c & b,r9 // r9,c )
reconsider a1 = a, b1 = b, c1 = c, p1 = p, p19 = p9, q1 = q, q19 = q9 as Element of the WeakAffVect ;
A26: ( a1,p1 '||' p1,b1 & a1,q1 '||' q1,c1 ) by A24, Lm15;
A27: ( a1,p19 '||' p19,b1 & a1,q19 '||' q19,c1 ) by A25, Lm15;
( a1,b1 '||' p1,p19 & a1,c1 '||' q1,q19 ) by A23, Lm15;
then consider r1, r19 being Element of the WeakAffVect such that
A28: ( b1,c1 '||' r1,r19 & b1,r1 '||' r1,c1 ) and
A29: b1,r19 '||' r19,c1 by A26, A27, Lm12;
reconsider r = r1, r9 = r19 as Element of AffinStruct(# the carrier of the WeakAffVect,P #) ;
A30: b,r9 // r9,c by A29, Lm15;
( b,c // r,r9 & b,r // r,c ) by A28, Lm15;
hence ex r, r9 being Element of AffinStruct(# the carrier of the WeakAffVect,P #) st
( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) by A30; :: thesis: verum

end;

end;

definition

let IT be non empty AffinStruct ;

attr IT is WeakAffSegm-like means :Def1: :: AFVECT01:def 1
( ( for a, b being Element of IT holds a,b // b,a ) & ( for a, b being Element of IT st a,b // a,a holds
a = b ) & ( for a, b, c, d, p, q being Element of IT st a,b // p,q & c,d // p,q holds
a,b // c,d ) & ( for a, c being Element of IT ex b being Element of IT st a,b // b,c ) & ( for a, a9, b, b9, p being Element of IT st a <> a9 & b <> b9 & p,a // p,a9 & p,b // p,b9 holds
a,b // a9,b9 ) & ( for a, b being Element of IT holds
( a = b or ex c being Element of IT st
( ( a <> c & a,b // b,c ) or ex p, p9 being Element of IT st
( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) ) ) & ( for a, b, b9, p, p9, c being Element of IT st a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 holds
a,b9 // b9,c ) & ( for a, b, b9, c being Element of IT st a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c holds
ex p, p9 being Element of IT st
( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) ) & ( for a, b, c, p, p9, q, q9 being Element of IT st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds
ex r, r9 being Element of IT st
( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) ) );

end;

:: deftheorem Def1 defines WeakAffSegm-like AFVECT01:def 1 :
for IT being non empty AffinStruct holds
( IT is WeakAffSegm-like iff ( ( for a, b being Element of IT holds a,b // b,a ) & ( for a, b being Element of IT st a,b // a,a holds
a = b ) & ( for a, b, c, d, p, q being Element of IT st a,b // p,q & c,d // p,q holds
a,b // c,d ) & ( for a, c being Element of IT ex b being Element of IT st a,b // b,c ) & ( for a, a9, b, b9, p being Element of IT st a <> a9 & b <> b9 & p,a // p,a9 & p,b // p,b9 holds
a,b // a9,b9 ) & ( for a, b being Element of IT holds
( a = b or ex c being Element of IT st
( ( a <> c & a,b // b,c ) or ex p, p9 being Element of IT st
( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) ) ) & ( for a, b, b9, p, p9, c being Element of IT st a,b // b,c & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 holds
a,b9 // b9,c ) & ( for a, b, b9, c being Element of IT st a <> c & b <> b9 & a,b // b,c & a,b9 // b9,c holds
ex p, p9 being Element of IT st
( p <> p9 & b,b9 // p,p9 & b,p // p,b9 & b,p9 // p9,b9 ) ) & ( for a, b, c, p, p9, q, q9 being Element of IT st a,b // p,p9 & a,c // q,q9 & a,p // p,b & a,q // q,c & a,p9 // p9,b & a,q9 // q9,c holds
ex r, r9 being Element of IT st
( b,c // r,r9 & b,r // r,c & b,r9 // r9,c ) ) ) );

registration

cluster non empty non trivial strict WeakAffSegm-like for AffinStruct ;

existence
ex b₁ being non trivial AffinStruct st
( b₁ is strict & b₁ is WeakAffSegm-like )

proof end;

end;

definition

mode WeakAffSegm is non trivial WeakAffSegm-like AffinStruct ;

end;

theorem Th1: :: AFVECT01:1

for AFV being WeakAffSegm
for a, b being Element of AFV holds a,b // a,b

proof end;

theorem Th2: :: AFVECT01:2

for AFV being WeakAffSegm
for a, b, c, d being Element of AFV st a,b // c,d holds
c,d // a,b

proof end;

theorem Th3: :: AFVECT01:3

for AFV being WeakAffSegm
for a, b, c, d being Element of AFV st a,b // c,d holds
a,b // d,c

proof end;

theorem Th4: :: AFVECT01:4

for AFV being WeakAffSegm
for a, b, c, d being Element of AFV st a,b // c,d holds
b,a // c,d

proof end;

theorem Th5: :: AFVECT01:5

for AFV being WeakAffSegm
for a, b being Element of AFV holds a,a // b,b

proof end;

theorem Th6: :: AFVECT01:6

for AFV being WeakAffSegm
for a, b, c being Element of AFV st a,b // c,c holds
a = b

proof end;

theorem Th7: :: AFVECT01:7

for AFV being WeakAffSegm
for a, b, c, p, p9 being Element of AFV st a,b // p,p9 & a,b // b,c & a,p // p,b & a,p9 // p9,b holds
a = c

proof end;

theorem :: AFVECT01:8

for AFV being WeakAffSegm
for a, b, b9, b99 being Element of AFV st a,b9 // a,b99 & a,b // a,b99 & not b = b9 & not b = b99 holds
b9 = b99

proof end;

::
:: RELATION OF MAXIMAL DISTANCE AND MIDPOINT RELATION
::

definition

let AFV be WeakAffSegm;
let a, b be Element of AFV;

pred MDist a,b means :: AFVECT01:def 2
ex p, p9 being Element of AFV st
( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b );

end;

:: deftheorem defines MDist AFVECT01:def 2 :
for AFV being WeakAffSegm
for a, b being Element of AFV holds
( MDist a,b iff ex p, p9 being Element of AFV st
( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) );

definition

let AFV be WeakAffSegm;
let a, b, c be Element of AFV;

pred Mid a,b,c means :: AFVECT01:def 3
( ( a = b & b = c & a = c ) or ( a = c & MDist a,b ) or ( a <> c & a,b // b,c ) );

end;

:: deftheorem defines Mid AFVECT01:def 3 :
for AFV being WeakAffSegm
for a, b, c being Element of AFV holds
( Mid a,b,c iff ( ( a = b & b = c & a = c ) or ( a = c & MDist a,b ) or ( a <> c & a,b // b,c ) ) );

theorem :: AFVECT01:9

for AFV being WeakAffSegm
for a, b being Element of AFV st a <> b & not MDist a,b holds
ex c being Element of AFV st
( a <> c & a,b // b,c ) by Def1;

theorem :: AFVECT01:10

for AFV being WeakAffSegm
for a, b, c being Element of AFV st MDist a,b & a,b // b,c holds
a = c by Th7;

theorem :: AFVECT01:11

for AFV being WeakAffSegm
for a, b being Element of AFV st MDist a,b holds
a <> b by Th2, Th6;