:: AFVECT01 semantic presentation

registration
let c1 be non empty set ;
let c2 be Relation of [:c1,c1:];
cluster AffinStruct(# a1,a2 #) -> non empty ;
coherence
not AffinStruct(# c1,c2 #) is empty by STRUCT_0:def 1;
end;

Lemma1: for b1 being WeakAffVect
for b2, b3, b4 being Element of b1 st b2,b3 '||' b3,b4 & b2 <> b4 holds
b2,b3 // b3,b4
proof end;

Lemma2: for b1 being WeakAffVect
for b2, b3 being Element of b1 holds
( b2,b3 // b3,b2 iff ex b4, b5 being Element of b1 st
( b2,b3 '||' b4,b5 & b2,b4 '||' b4,b3 & b2,b5 '||' b5,b3 ) )
proof end;

Lemma3: for b1 being WeakAffVect
for b2, b3, b4, b5 being Element of b1 st b2,b3 '||' b4,b5 holds
b3,b2 '||' b4,b5
proof end;

Lemma4: for b1 being WeakAffVect
for b2, b3 being Element of b1 holds b2,b3 '||' b3,b2
proof end;

Lemma5: for b1 being WeakAffVect
for b2, b3, b4 being Element of b1 st b2,b3 '||' b4,b4 holds
b2 = b3
proof end;

Lemma6: for b1 being WeakAffVect
for b2, b3, b4, b5, b6, b7 being Element of b1 st b2,b3 '||' b6,b7 & b4,b5 '||' b6,b7 holds
b2,b3 '||' b4,b5
proof end;

Lemma7: for b1 being WeakAffVect
for b2, b3 being Element of b1 ex b4 being Element of b1 st b2,b4 '||' b4,b3
proof end;

Lemma8: for b1 being WeakAffVect
for b2, b3, b4, b5, b6 being Element of b1 st b2 <> b3 & b4 <> b5 & b6,b2 '||' b6,b3 & b6,b4 '||' b6,b5 holds
b2,b4 '||' b3,b5
proof end;

Lemma9: for b1 being WeakAffVect
for b2, b3 being Element of b1 holds
( b2 = b3 or ex b4 being Element of b1 st
( ( b2 <> b4 & b2,b3 '||' b3,b4 ) or ex b5, b6 being Element of b1 st
( b5 <> b6 & b2,b3 '||' b5,b6 & b2,b5 '||' b5,b3 & b2,b6 '||' b6,b3 ) ) )
proof end;

Lemma10: for b1 being WeakAffVect
for b2, b3, b4, b5, b6, b7 being Element of b1 st b2,b3 '||' b3,b7 & b3,b4 '||' b5,b6 & b3,b5 '||' b5,b4 & b3,b6 '||' b6,b4 holds
b2,b4 '||' b4,b7
proof end;

Lemma11: for b1 being WeakAffVect
for b2, b3, b4, b5 being Element of b1 st b2 <> b5 & b3 <> b4 & b2,b3 '||' b3,b5 & b2,b4 '||' b4,b5 holds
ex b6, b7 being Element of b1 st
( b6 <> b7 & b3,b4 '||' b6,b7 & b3,b6 '||' b6,b4 & b3,b7 '||' b7,b4 )
proof end;

Lemma12: for b1 being WeakAffVect
for b2, b3, b4, b5, b6, b7, b8 being Element of b1 st b2,b3 '||' b5,b6 & b2,b4 '||' b7,b8 & b2,b5 '||' b5,b3 & b2,b7 '||' b7,b4 & b2,b6 '||' b6,b3 & b2,b8 '||' b8,b4 holds
ex b9, b10 being Element of b1 st
( b3,b4 '||' b9,b10 & b3,b9 '||' b9,b4 & b3,b10 '||' b10,b4 )
proof end;

consider c1 being WeakAffVect;

set c2 = the carrier of c1;

set c3 = [:the carrier of c1,the carrier of c1:];

defpred S1[ set , set ] means ex b1, b2, b3, b4 being Element of the carrier of c1 st
( a1 = [b1,b2] & a2 = [b3,b4] & b1,b2 '||' b3,b4 );

consider c4 being Relation of [:the carrier of c1,the carrier of c1:],[:the carrier of c1,the carrier of c1:] such that
Lemma13: for b1, b2 being set holds
( [b1,b2] in c4 iff ( b1 in [:the carrier of c1,the carrier of c1:] & b2 in [:the carrier of c1,the carrier of c1:] & S1[b1,b2] ) ) from RELSET_1:sch 1();

Lemma14: for b1, b2, b3, b4 being Element of the carrier of c1 holds
( [[b1,b2],[b3,b4]] in c4 iff b1,b2 '||' b3,b4 )
proof end;

set c5 = AffinStruct(# the carrier of c1,c4 #);

Lemma15: for b1, b2, b3, b4 being Element of c1
for b5, b6, b7, b8 being Element of the carrier of AffinStruct(# the carrier of c1,c4 #) st b1 = b5 & b2 = b6 & b3 = b7 & b4 = b8 holds
( b1,b2 '||' b3,b4 iff b5,b6 // b7,b8 )
proof end;

E16: now
thus ex b1, b2 being Element of AffinStruct(# the carrier of c1,c4 #) st b1 <> b2 by REALSET2:def 7;
thus for b1, b2 being Element of AffinStruct(# the carrier of c1,c4 #) holds b1,b2 // b2,b1
proof
let c6, c7 be Element of AffinStruct(# the carrier of c1,c4 #);
reconsider c8 = c6, c9 = c7 as Element of the carrier of c1 ;
c8,c9 '||' c9,c8 by Lemma4;
hence c6,c7 // c7,c6 by Lemma15;
end;
thus for b1, b2 being Element of AffinStruct(# the carrier of c1,c4 #) st b1,b2 // b1,b1 holds
b1 = b2
proof
let c6, c7 be Element of AffinStruct(# the carrier of c1,c4 #);
assume E17: c6,c7 // c6,c6 ;
reconsider c8 = c6, c9 = c7 as Element of c1 ;
c8,c9 '||' c8,c8 by E17, Lemma15;
hence c6 = c7 by Lemma5;
end;
thus for b1, b2, b3, b4, b5, b6 being Element of AffinStruct(# the carrier of c1,c4 #) st b1,b2 // b5,b6 & b3,b4 // b5,b6 holds
b1,b2 // b3,b4
proof
let c6, c7, c8, c9, c10, c11 be Element of AffinStruct(# the carrier of c1,c4 #);
assume E17: ( c6,c7 // c10,c11 & c8,c9 // c10,c11 ) ;
reconsider c12 = c6, c13 = c7, c14 = c8, c15 = c9, c16 = c10, c17 = c11 as Element of c1 ;
( c12,c13 '||' c16,c17 & c14,c15 '||' c16,c17 ) by E17, Lemma15;
then c12,c13 '||' c14,c15 by Lemma6;
hence c6,c7 // c8,c9 by Lemma15;
end;
thus for b1, b2 being Element of AffinStruct(# the carrier of c1,c4 #) ex b3 being Element of the carrier of AffinStruct(# the carrier of c1,c4 #) st b1,b3 // b3,b2
proof
let c6, c7 be Element of AffinStruct(# the carrier of c1,c4 #);
reconsider c8 = c6, c9 = c7 as Element of c1 ;
consider c10 being Element of c1 such that
E17: c8,c10 '||' c10,c9 by Lemma7;
reconsider c11 = c10 as Element of AffinStruct(# the carrier of c1,c4 #) ;
c6,c11 // c11,c7 by E17, Lemma15;
hence ex b1 being Element of the carrier of AffinStruct(# the carrier of c1,c4 #) st c6,b1 // b1,c7 ;
end;
thus for b1, b2, b3, b4, b5 being Element of AffinStruct(# the carrier of c1,c4 #) st b1 <> b2 & b3 <> b4 & b5,b1 // b5,b2 & b5,b3 // b5,b4 holds
b1,b3 // b2,b4
proof
let c6, c7, c8, c9, c10 be Element of AffinStruct(# the carrier of c1,c4 #);
assume that
E17: ( c6 <> c7 & c8 <> c9 ) and
E18: ( c10,c6 // c10,c7 & c10,c8 // c10,c9 ) ;
reconsider c11 = c6, c12 = c7, c13 = c8, c14 = c9, c15 = c10 as Element of c1 ;
( c15,c11 '||' c15,c12 & c15,c13 '||' c15,c14 ) by E18, Lemma15;
then c11,c13 '||' c12,c14 by E17, Lemma8;
hence c6,c8 // c7,c9 by Lemma15;
end;
thus for b1, b2 being Element of AffinStruct(# the carrier of c1,c4 #) holds
( b1 = b2 or ex b3 being Element of AffinStruct(# the carrier of c1,c4 #) st
( ( b1 <> b3 & b1,b2 // b2,b3 ) or ex b4, b5 being Element of AffinStruct(# the carrier of c1,c4 #) st
( b4 <> b5 & b1,b2 // b4,b5 & b1,b4 // b4,b2 & b1,b5 // b5,b2 ) ) )
proof
let c6, c7 be Element of AffinStruct(# the carrier of c1,c4 #);
assume E17: not c6 = c7 ;
reconsider c8 = c6, c9 = c7 as Element of c1 ;
E18: now
given c10 being Element of c1 such that E19: ( c8 <> c10 & c8,c9 '||' c9,c10 ) ;
reconsider c11 = c10 as Element of AffinStruct(# the carrier of c1,c4 #) ;
( c6 <> c11 & c6,c7 // c7,c11 ) by E19, Lemma15;
hence ex b1 being Element of AffinStruct(# the carrier of c1,c4 #) st
( c6 <> b1 & c6,c7 // c7,b1 ) ;
end;
now
given c10, c11 being Element of c1 such that E19: ( c10 <> c11 & c8,c9 '||' c10,c11 & c8,c10 '||' c10,c9 & c8,c11 '||' c11,c9 ) ;
reconsider c12 = c10, c13 = c11 as Element of AffinStruct(# the carrier of c1,c4 #) ;
( c12 <> c13 & c6,c7 // c12,c13 & c6,c12 // c12,c7 & c6,c13 // c13,c7 ) by E19, Lemma15;
hence ex b1, b2 being Element of AffinStruct(# the carrier of c1,c4 #) st
( b1 <> b2 & c6,c7 // b1,b2 & c6,b1 // b1,c7 & c6,b2 // b2,c7 ) ;
end;
hence ex b1 being Element of AffinStruct(# the carrier of c1,c4 #) st
( ( c6 <> b1 & c6,c7 // c7,b1 ) or ex b2, b3 being Element of AffinStruct(# the carrier of c1,c4 #) st
( b2 <> b3 & c6,c7 // b2,b3 & c6,b2 // b2,c7 & c6,b3 // b3,c7 ) ) by E17, E18, Lemma9;
end;
thus for b1, b2, b3, b4, b5, b6 being Element of AffinStruct(# the carrier of c1,c4 #) st b1,b2 // b2,b6 & b2,b3 // b4,b5 & b2,b4 // b4,b3 & b2,b5 // b5,b3 holds
b1,b3 // b3,b6
proof
let c6, c7, c8, c9, c10, c11 be Element of AffinStruct(# the carrier of c1,c4 #);
assume E17: ( c6,c7 // c7,c11 & c7,c8 // c9,c10 & c7,c9 // c9,c8 & c7,c10 // c10,c8 ) ;
reconsider c12 = c6, c13 = c7, c14 = c8, c15 = c9, c16 = c10, c17 = c11 as Element of c1 ;
( c12,c13 '||' c13,c17 & c13,c14 '||' c15,c16 & c13,c15 '||' c15,c14 & c13,c16 '||' c16,c14 ) by E17, Lemma15;
then c12,c14 '||' c14,c17 by Lemma10;
hence c6,c8 // c8,c11 by Lemma15;
end;
thus for b1, b2, b3, b4 being Element of AffinStruct(# the carrier of c1,c4 #) st b1 <> b4 & b2 <> b3 & b1,b2 // b2,b4 & b1,b3 // b3,b4 holds
ex b5, b6 being Element of AffinStruct(# the carrier of c1,c4 #) st
( b5 <> b6 & b2,b3 // b5,b6 & b2,b5 // b5,b3 & b2,b6 // b6,b3 )
proof
let c6, c7, c8, c9 be Element of AffinStruct(# the carrier of c1,c4 #);
assume that
E17: ( c6 <> c9 & c7 <> c8 ) and
E18: ( c6,c7 // c7,c9 & c6,c8 // c8,c9 ) ;
reconsider c10 = c6, c11 = c7, c12 = c8, c13 = c9 as Element of the carrier of c1 ;
( c10,c11 '||' c11,c13 & c10,c12 '||' c12,c13 ) by E18, Lemma15;
then consider c14, c15 being Element of c1 such that
E19: ( c14 <> c15 & c11,c12 '||' c14,c15 & c11,c14 '||' c14,c12 & c11,c15 '||' c15,c12 ) by E17, Lemma11;
reconsider c16 = c14, c17 = c15 as Element of AffinStruct(# the carrier of c1,c4 #) ;
( c16 <> c17 & c7,c8 // c16,c17 & c7,c16 // c16,c8 & c7,c17 // c17,c8 ) by E19, Lemma15;
hence ex b1, b2 being Element of AffinStruct(# the carrier of c1,c4 #) st
( b1 <> b2 & c7,c8 // b1,b2 & c7,b1 // b1,c8 & c7,b2 // b2,c8 ) ;
end;
thus for b1, b2, b3, b4, b5, b6, b7 being Element of AffinStruct(# the carrier of c1,c4 #) st b1,b2 // b4,b5 & b1,b3 // b6,b7 & b1,b4 // b4,b2 & b1,b6 // b6,b3 & b1,b5 // b5,b2 & b1,b7 // b7,b3 holds
ex b8, b9 being Element of AffinStruct(# the carrier of c1,c4 #) st
( b2,b3 // b8,b9 & b2,b8 // b8,b3 & b2,b9 // b9,b3 )
proof
let c6, c7, c8, c9, c10, c11, c12 be Element of AffinStruct(# the carrier of c1,c4 #);
assume E17: ( c6,c7 // c9,c10 & c6,c8 // c11,c12 & c6,c9 // c9,c7 & c6,c11 // c11,c8 & c6,c10 // c10,c7 & c6,c12 // c12,c8 ) ;
reconsider c13 = c6, c14 = c7, c15 = c8, c16 = c9, c17 = c10, c18 = c11, c19 = c12 as Element of the carrier of c1 ;
( c13,c14 '||' c16,c17 & c13,c15 '||' c18,c19 & c13,c16 '||' c16,c14 & c13,c18 '||' c18,c15 & c13,c17 '||' c17,c14 & c13,c19 '||' c19,c15 ) by E17, Lemma15;
then consider c20, c21 being Element of c1 such that
E18: ( c14,c15 '||' c20,c21 & c14,c20 '||' c20,c15 & c14,c21 '||' c21,c15 ) by Lemma12;
reconsider c22 = c20, c23 = c21 as Element of AffinStruct(# the carrier of c1,c4 #) ;
( c7,c8 // c22,c23 & c7,c22 // c22,c8 & c7,c23 // c23,c8 ) by E18, Lemma15;
hence ex b1, b2 being Element of AffinStruct(# the carrier of c1,c4 #) st
( c7,c8 // b1,b2 & c7,b1 // b1,c8 & c7,b2 // b2,c8 ) ;
end;
end;

definition
let c6 be non empty AffinStruct ;
canceled;
attr a1 is WeakAffSegm-like means :Def2: :: AFVECT01:def 2
( ( for b1, b2 being Element of a1 holds b1,b2 // b2,b1 ) & ( for b1, b2 being Element of a1 st b1,b2 // b1,b1 holds
b1 = b2 ) & ( for b1, b2, b3, b4, b5, b6 being Element of a1 st b1,b2 // b5,b6 & b3,b4 // b5,b6 holds
b1,b2 // b3,b4 ) & ( for b1, b2 being Element of a1 ex b3 being Element of a1 st b1,b3 // b3,b2 ) & ( for b1, b2, b3, b4, b5 being Element of a1 st b1 <> b2 & b3 <> b4 & b5,b1 // b5,b2 & b5,b3 // b5,b4 holds
b1,b3 // b2,b4 ) & ( for b1, b2 being Element of a1 holds
( b1 = b2 or ex b3 being Element of a1 st
( ( b1 <> b3 & b1,b2 // b2,b3 ) or ex b4, b5 being Element of a1 st
( b4 <> b5 & b1,b2 // b4,b5 & b1,b4 // b4,b2 & b1,b5 // b5,b2 ) ) ) ) & ( for b1, b2, b3, b4, b5, b6 being Element of a1 st b1,b2 // b2,b6 & b2,b3 // b4,b5 & b2,b4 // b4,b3 & b2,b5 // b5,b3 holds
b1,b3 // b3,b6 ) & ( for b1, b2, b3, b4 being Element of a1 st b1 <> b4 & b2 <> b3 & b1,b2 // b2,b4 & b1,b3 // b3,b4 holds
ex b5, b6 being Element of a1 st
( b5 <> b6 & b2,b3 // b5,b6 & b2,b5 // b5,b3 & b2,b6 // b6,b3 ) ) & ( for b1, b2, b3, b4, b5, b6, b7 being Element of a1 st b1,b2 // b4,b5 & b1,b3 // b6,b7 & b1,b4 // b4,b2 & b1,b6 // b6,b3 & b1,b5 // b5,b2 & b1,b7 // b7,b3 holds
ex b8, b9 being Element of a1 st
( b2,b3 // b8,b9 & b2,b8 // b8,b3 & b2,b9 // b9,b3 ) ) );
end;

:: deftheorem Def1 AFVECT01:def 1 :
canceled;

:: deftheorem Def2 defines WeakAffSegm-like AFVECT01:def 2 :
for b1 being non empty AffinStruct holds
( b1 is WeakAffSegm-like iff ( ( for b2, b3 being Element of b1 holds b2,b3 // b3,b2 ) & ( for b2, b3 being Element of b1 st b2,b3 // b2,b2 holds
b2 = b3 ) & ( for b2, b3, b4, b5, b6, b7 being Element of b1 st b2,b3 // b6,b7 & b4,b5 // b6,b7 holds
b2,b3 // b4,b5 ) & ( for b2, b3 being Element of b1 ex b4 being Element of b1 st b2,b4 // b4,b3 ) & ( for b2, b3, b4, b5, b6 being Element of b1 st b2 <> b3 & b4 <> b5 & b6,b2 // b6,b3 & b6,b4 // b6,b5 holds
b2,b4 // b3,b5 ) & ( for b2, b3 being Element of b1 holds
( b2 = b3 or ex b4 being Element of b1 st
( ( b2 <> b4 & b2,b3 // b3,b4 ) or ex b5, b6 being Element of b1 st
( b5 <> b6 & b2,b3 // b5,b6 & b2,b5 // b5,b3 & b2,b6 // b6,b3 ) ) ) ) & ( for b2, b3, b4, b5, b6, b7 being Element of b1 st b2,b3 // b3,b7 & b3,b4 // b5,b6 & b3,b5 // b5,b4 & b3,b6 // b6,b4 holds
b2,b4 // b4,b7 ) & ( for b2, b3, b4, b5 being Element of b1 st b2 <> b5 & b3 <> b4 & b2,b3 // b3,b5 & b2,b4 // b4,b5 holds
ex b6, b7 being Element of b1 st
( b6 <> b7 & b3,b4 // b6,b7 & b3,b6 // b6,b4 & b3,b7 // b7,b4 ) ) & ( for b2, b3, b4, b5, b6, b7, b8 being Element of b1 st b2,b3 // b5,b6 & b2,b4 // b7,b8 & b2,b5 // b5,b3 & b2,b7 // b7,b4 & b2,b6 // b6,b3 & b2,b8 // b8,b4 holds
ex b9, b10 being Element of b1 st
( b3,b4 // b9,b10 & b3,b9 // b9,b4 & b3,b10 // b10,b4 ) ) ) );

registration
cluster non empty non trivial strict WeakAffSegm-like AffinStruct ;
existence
ex b1 being non empty AffinStruct st
( b1 is strict & not b1 is trivial & b1 is WeakAffSegm-like )
proof end;
end;

definition
mode WeakAffSegm is non empty non trivial WeakAffSegm-like AffinStruct ;
end;

theorem Th1: :: AFVECT01:1
for b1 being WeakAffSegm
for b2, b3 being Element of b1 holds b2,b3 // b2,b3
proof end;

theorem Th2: :: AFVECT01:2
for b1 being WeakAffSegm
for b2, b3, b4, b5 being Element of b1 st b2,b3 // b4,b5 holds
b4,b5 // b2,b3
proof end;

theorem Th3: :: AFVECT01:3
for b1 being WeakAffSegm
for b2, b3, b4, b5 being Element of b1 st b2,b3 // b4,b5 holds
b2,b3 // b5,b4
proof end;

theorem Th4: :: AFVECT01:4
for b1 being WeakAffSegm
for b2, b3, b4, b5 being Element of b1 st b2,b3 // b4,b5 holds
b3,b2 // b4,b5
proof end;

theorem Th5: :: AFVECT01:5
for b1 being WeakAffSegm
for b2, b3 being Element of b1 holds b2,b2 // b3,b3
proof end;

theorem Th6: :: AFVECT01:6
for b1 being WeakAffSegm
for b2, b3, b4 being Element of b1 st b2,b3 // b4,b4 holds
b2 = b3
proof end;

theorem Th7: :: AFVECT01:7
for b1 being WeakAffSegm
for b2, b3, b4, b5, b6 being Element of b1 st b2,b3 // b4,b5 & b2,b3 // b3,b6 & b2,b4 // b4,b3 & b2,b5 // b5,b3 holds
b2 = b6
proof end;

theorem Th8: :: AFVECT01:8
for b1 being WeakAffSegm
for b2, b3, b4, b5 being Element of b1 st b2,b3 // b2,b4 & b2,b5 // b2,b4 & not b5 = b3 & not b5 = b4 holds
b3 = b4
proof end;

definition
let c6 be WeakAffSegm;
let c7, c8 be Element of c6;
canceled;
pred MDist c2,c3 means :Def4: :: AFVECT01:def 4
ex b1, b2 being Element of a1 st
( b1 <> b2 & a2,a3 // b1,b2 & a2,b1 // b1,a3 & a2,b2 // b2,a3 );
end;

:: deftheorem Def3 AFVECT01:def 3 :
canceled;

:: deftheorem Def4 defines MDist AFVECT01:def 4 :
for b1 being WeakAffSegm
for b2, b3 being Element of b1 holds
( MDist b2,b3 iff ex b4, b5 being Element of b1 st
( b4 <> b5 & b2,b3 // b4,b5 & b2,b4 // b4,b3 & b2,b5 // b5,b3 ) );

definition
let c6 be WeakAffSegm;
let c7, c8, c9 be Element of c6;
pred Mid c2,c3,c4 means :: AFVECT01:def 5
( ( a2 = a3 & a3 = a4 & a2 = a4 ) or ( a2 = a4 & MDist a2,a3 ) or ( a2 <> a4 & a2,a3 // a3,a4 ) );
end;

:: deftheorem Def5 defines Mid AFVECT01:def 5 :
for b1 being WeakAffSegm
for b2, b3, b4 being Element of b1 holds
( Mid b2,b3,b4 iff ( ( b2 = b3 & b3 = b4 & b2 = b4 ) or ( b2 = b4 & MDist b2,b3 ) or ( b2 <> b4 & b2,b3 // b3,b4 ) ) );

theorem Th9: :: AFVECT01:9
canceled;

theorem Th10: :: AFVECT01:10
canceled;

theorem Th11: :: AFVECT01:11
for b1 being WeakAffSegm
for b2, b3 being Element of b1 st b2 <> b3 & not MDist b2,b3 holds
ex b4 being Element of b1 st
( b2 <> b4 & b2,b3 // b3,b4 )
proof end;

theorem Th12: :: AFVECT01:12
for b1 being WeakAffSegm
for b2, b3, b4 being Element of b1 st MDist b2,b3 & b2,b3 // b3,b4 holds
b2 = b4
proof end;

theorem Th13: :: AFVECT01:13
for b1 being WeakAffSegm
for b2, b3 being Element of b1 st MDist b2,b3 holds
b2 <> b3
proof end;