:: One-Dimensional Congruence of Segments, Basic Facts and Midpoint RelationKrzysztof Pra\.zmowski
:: by Barbara Konstanta, Urszula Kowieska, Grzegorz Lewandowski and
::
:: Received October 4, 1990
:: Copyright (c) 1990 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, a', b, b', p being Element of AFV st a <> a' & b <> b' & p,a '||' p,a' & p,b '||' p,b' holds
a,b '||' a',b'

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, p' being Element of AFV st
( p <> p' & a,b '||' p,p' & a,p '||' p,b & a,p' '||' p',b ) ) )

proof end;

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

proof end;

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

proof end;

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

proof end;

consider AFV0 being WeakAffVect;

set X = the carrier of AFV0;

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

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

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

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

proof end;

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

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

proof end;

Lm16: now

thus ex a', b' being Element of AffinStruct(# the carrier of AFV0,P #) st a' <> b' by STRUCT_0:def 10; :: thesis: ( ( for a', b' being Element of AffinStruct(# the carrier of AFV0,P #) holds a',b' // b',a' ) & ( for a', b' being Element of AffinStruct(# the carrier of AFV0,P #) st a',b' // a',a' holds
a' = b' ) & ( for a, b, c, d, p, q being Element of AffinStruct(# the carrier of AFV0,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 AFV0,P #) ex b being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c ) & ( for a, a', b, b', p being Element of AffinStruct(# the carrier of AFV0,P #) st a <> a' & b <> b' & p,a // p,a' & p,b // p,b' holds
a,b // a',b' ) & ( for a, b being Element of AffinStruct(# the carrier of AFV0,P #) holds
( a = b or ex c being Element of AffinStruct(# the carrier of AFV0,P #) st
( ( a <> c & a,b // b,c ) or ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) ) ) ) & ( for a, b, b', p, p', c being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c & b,b' // p,p' & b,p // p,b' & b,p' // p',b' holds
a,b' // b',c ) & ( for a, b, b', c being Element of AffinStruct(# the carrier of AFV0,P #) st a <> c & b <> b' & a,b // b,c & a,b' // b',c holds
ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & b,b' // p,p' & b,p // p,b' & b,p' // p',b' ) ) & ( for a, b, c, p, p', q, q' being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // p,p' & a,c // q,q' & a,p // p,b & a,q // q,c & a,p' // p',b & a,q' // q',c holds
ex r, r' being Element of AffinStruct(# the carrier of AFV0,P #) st
( b,c // r,r' & b,r // r,c & b,r' // r',c ) ) )
thus for a', b' being Element of AffinStruct(# the carrier of AFV0,P #) holds a',b' // b',a' :: thesis: ( ( for a', b' being Element of AffinStruct(# the carrier of AFV0,P #) st a',b' // a',a' holds
a' = b' ) & ( for a, b, c, d, p, q being Element of AffinStruct(# the carrier of AFV0,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 AFV0,P #) ex b being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c ) & ( for a, a', b, b', p being Element of AffinStruct(# the carrier of AFV0,P #) st a <> a' & b <> b' & p,a // p,a' & p,b // p,b' holds
a,b // a',b' ) & ( for a, b being Element of AffinStruct(# the carrier of AFV0,P #) holds
( a = b or ex c being Element of AffinStruct(# the carrier of AFV0,P #) st
( ( a <> c & a,b // b,c ) or ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) ) ) ) & ( for a, b, b', p, p', c being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c & b,b' // p,p' & b,p // p,b' & b,p' // p',b' holds
a,b' // b',c ) & ( for a, b, b', c being Element of AffinStruct(# the carrier of AFV0,P #) st a <> c & b <> b' & a,b // b,c & a,b' // b',c holds
ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & b,b' // p,p' & b,p // p,b' & b,p' // p',b' ) ) & ( for a, b, c, p, p', q, q' being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // p,p' & a,c // q,q' & a,p // p,b & a,q // q,c & a,p' // p',b & a,q' // q',c holds
ex r, r' being Element of AffinStruct(# the carrier of AFV0,P #) st
( b,c // r,r' & b,r // r,c & b,r' // r',c ) ) )

proof

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

end;

thus for a', b' being Element of AffinStruct(# the carrier of AFV0,P #) st a',b' // a',a' holds
a' = b' :: thesis: ( ( for a, b, c, d, p, q being Element of AffinStruct(# the carrier of AFV0,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 AFV0,P #) ex b being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c ) & ( for a, a', b, b', p being Element of AffinStruct(# the carrier of AFV0,P #) st a <> a' & b <> b' & p,a // p,a' & p,b // p,b' holds
a,b // a',b' ) & ( for a, b being Element of AffinStruct(# the carrier of AFV0,P #) holds
( a = b or ex c being Element of AffinStruct(# the carrier of AFV0,P #) st
( ( a <> c & a,b // b,c ) or ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) ) ) ) & ( for a, b, b', p, p', c being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c & b,b' // p,p' & b,p // p,b' & b,p' // p',b' holds
a,b' // b',c ) & ( for a, b, b', c being Element of AffinStruct(# the carrier of AFV0,P #) st a <> c & b <> b' & a,b // b,c & a,b' // b',c holds
ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & b,b' // p,p' & b,p // p,b' & b,p' // p',b' ) ) & ( for a, b, c, p, p', q, q' being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // p,p' & a,c // q,q' & a,p // p,b & a,q // q,c & a,p' // p',b & a,q' // q',c holds
ex r, r' being Element of AffinStruct(# the carrier of AFV0,P #) st
( b,c // r,r' & b,r // r,c & b,r' // r',c ) ) )

proof

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

end;

thus for a, b, c, d, p, q being Element of AffinStruct(# the carrier of AFV0,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 AFV0,P #) ex b being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c ) & ( for a, a', b, b', p being Element of AffinStruct(# the carrier of AFV0,P #) st a <> a' & b <> b' & p,a // p,a' & p,b // p,b' holds
a,b // a',b' ) & ( for a, b being Element of AffinStruct(# the carrier of AFV0,P #) holds
( a = b or ex c being Element of AffinStruct(# the carrier of AFV0,P #) st
( ( a <> c & a,b // b,c ) or ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) ) ) ) & ( for a, b, b', p, p', c being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c & b,b' // p,p' & b,p // p,b' & b,p' // p',b' holds
a,b' // b',c ) & ( for a, b, b', c being Element of AffinStruct(# the carrier of AFV0,P #) st a <> c & b <> b' & a,b // b,c & a,b' // b',c holds
ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & b,b' // p,p' & b,p // p,b' & b,p' // p',b' ) ) & ( for a, b, c, p, p', q, q' being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // p,p' & a,c // q,q' & a,p // p,b & a,q // q,c & a,p' // p',b & a,q' // q',c holds
ex r, r' being Element of AffinStruct(# the carrier of AFV0,P #) st
( b,c // r,r' & b,r // r,c & b,r' // r',c ) ) )

proof

let a, b, c, d, p, q be Element of AffinStruct(# the carrier of AFV0,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 AFV0 ;
( 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 AFV0,P #) ex b being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c :: thesis: ( ( for a, a', b, b', p being Element of AffinStruct(# the carrier of AFV0,P #) st a <> a' & b <> b' & p,a // p,a' & p,b // p,b' holds
a,b // a',b' ) & ( for a, b being Element of AffinStruct(# the carrier of AFV0,P #) holds
( a = b or ex c being Element of AffinStruct(# the carrier of AFV0,P #) st
( ( a <> c & a,b // b,c ) or ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) ) ) ) & ( for a, b, b', p, p', c being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // b,c & b,b' // p,p' & b,p // p,b' & b,p' // p',b' holds
a,b' // b',c ) & ( for a, b, b', c being Element of AffinStruct(# the carrier of AFV0,P #) st a <> c & b <> b' & a,b // b,c & a,b' // b',c holds
ex p, p' being Element of AffinStruct(# the carrier of AFV0,P #) st
( p <> p' & b,b' // p,p' & b,p // p,b' & b,p' // p',b' ) ) & ( for a, b, c, p, p', q, q' being Element of AffinStruct(# the carrier of AFV0,P #) st a,b // p,p' & a,c // q,q' & a,p // p,b & a,q // q,c & a,p' // p',b & a,q' // q',c holds
ex r, r' being Element of AffinStruct(# the carrier of AFV0,P #) st
( b,c // r,r' & b,r // r,c & b,r' // r',c ) ) )

proof

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

end;

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

proof

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

end;

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

proof

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

A7: now

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

end;

now

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

end;

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

end;

definition

let IT be non empty AffinStruct ;
canceled;
attr IT is WeakAffSegm-like means :Def2: :: AFVECT01:def 2
( ( 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, a', b, b', p being Element of IT st a <> a' & b <> b' & p,a // p,a' & p,b // p,b' holds
a,b // a',b' ) & ( 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, p' being Element of IT st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) ) ) ) & ( for a, b, b', p, p', c being Element of IT st a,b // b,c & b,b' // p,p' & b,p // p,b' & b,p' // p',b' holds
a,b' // b',c ) & ( for a, b, b', c being Element of IT st a <> c & b <> b' & a,b // b,c & a,b' // b',c holds
ex p, p' being Element of IT st
( p <> p' & b,b' // p,p' & b,p // p,b' & b,p' // p',b' ) ) & ( for a, b, c, p, p', q, q' being Element of IT st a,b // p,p' & a,c // q,q' & a,p // p,b & a,q // q,c & a,p' // p',b & a,q' // q',c holds
ex r, r' being Element of IT st
( b,c // r,r' & b,r // r,c & b,r' // r',c ) ) );

end;

:: deftheorem AFVECT01:def 1 :

canceled;

:: deftheorem Def2 defines WeakAffSegm-like AFVECT01:def 2 :

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, a', b, b', p being Element of IT st a <> a' & b <> b' & p,a // p,a' & p,b // p,b' holds
a,b // a',b' ) & ( 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, p' being Element of IT st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) ) ) ) & ( for a, b, b', p, p', c being Element of IT st a,b // b,c & b,b' // p,p' & b,p // p,b' & b,p' // p',b' holds
a,b' // b',c ) & ( for a, b, b', c being Element of IT st a <> c & b <> b' & a,b // b,c & a,b' // b',c holds
ex p, p' being Element of IT st
( p <> p' & b,b' // p,p' & b,p // p,b' & b,p' // p',b' ) ) & ( for a, b, c, p, p', q, q' being Element of IT st a,b // p,p' & a,c // q,q' & a,p // p,b & a,q // q,c & a,p' // p',b & a,q' // q',c holds
ex r, r' being Element of IT st
( b,c // r,r' & b,r // r,c & b,r' // r',c ) ) ) );

registration

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

proof end;

end;

definition

mode WeakAffSegm is non empty 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, p, p', c being Element of AFV st a,b // p,p' & a,b // b,c & a,p // p,b & a,p' // p',b holds
a = c

proof end;

theorem :: AFVECT01:8

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

proof end;

definition

let AFV be WeakAffSegm;
let a, b be Element of AFV;
canceled;
pred MDist a,b means :Def4: :: AFVECT01:def 4
ex p, p' being Element of AFV st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b );

end;

:: deftheorem AFVECT01:def 3 :

canceled;

:: deftheorem Def4 defines MDist AFVECT01:def 4 :

for AFV being WeakAffSegm
for a, b being Element of AFV holds
( MDist a,b iff ex p, p' being Element of AFV st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) );

definition

let AFV be WeakAffSegm;
let a, b, c be Element of AFV;
pred Mid a,b,c means :: AFVECT01:def 5
( ( 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 5 :

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

canceled;

theorem :: AFVECT01:10

canceled;

theorem :: AFVECT01:11

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 )

proof end;

theorem :: AFVECT01:12

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

proof end;

theorem :: AFVECT01:13

for AFV being WeakAffSegm
for a, b being Element of AFV st MDist a,b holds
a <> b

proof end;