:: AFVECT0 semantic presentation

definition
let c1 be non empty AffinStruct ;
attr a1 is WeakAffVect-like means :Def1: :: AFVECT0:def 1
( ( for b1, b2, b3 being Element of a1 holds
( b1,b2 // b3,b3 implies b1 = b2 ) ) & ( for b1, b2, b3, b4, b5, b6 being Element of a1 holds
( b1,b2 // b5,b6 & b3,b4 // b5,b6 implies b1,b2 // b3,b4 ) ) & ( for b1, b2, b3 being Element of a1 holds
ex b4 being Element of a1 st b1,b2 // b3,b4 ) & ( for b1, b2, b3, b4, b5, b6 being Element of a1 holds
( b1,b2 // b4,b5 & b1,b3 // b4,b6 implies b2,b3 // b5,b6 ) ) & ( for b1, b2 being Element of a1 holds
ex b3 being Element of a1 st b1,b3 // b3,b2 ) & ( for b1, b2, b3, b4 being Element of a1 holds
( b1,b2 // b3,b4 implies b1,b3 // b2,b4 ) ) );
end;

:: deftheorem Def1 defines WeakAffVect-like AFVECT0:def 1 :
for b1 being non empty AffinStruct holds
( b1 is WeakAffVect-like iff ( ( for b2, b3, b4 being Element of b1 holds
( b2,b3 // b4,b4 implies b2 = b3 ) ) & ( for b2, b3, b4, b5, b6, b7 being Element of b1 holds
( b2,b3 // b6,b7 & b4,b5 // b6,b7 implies b2,b3 // b4,b5 ) ) & ( for b2, b3, b4 being Element of b1 holds
ex b5 being Element of b1 st b2,b3 // b4,b5 ) & ( for b2, b3, b4, b5, b6, b7 being Element of b1 holds
( b2,b3 // b5,b6 & b2,b4 // b5,b7 implies b3,b4 // b6,b7 ) ) & ( for b2, b3 being Element of b1 holds
ex b4 being Element of b1 st b2,b4 // b4,b3 ) & ( for b2, b3, b4, b5 being Element of b1 holds
( b2,b3 // b4,b5 implies b2,b4 // b3,b5 ) ) ) );

registration
cluster non empty non trivial strict WeakAffVect-like AffinStruct ;
existence
ex b1 being non empty AffinStruct st
( b1 is strict & not b1 is trivial & b1 is WeakAffVect-like )
proof
consider c1 being strict AffVect;
reconsider c2 = c1 as non empty AffinStruct ;
( ( for b1, b2, b3 being Element of c2 holds
( b1,b2 // b3,b3 implies b1 = b2 ) ) & ( for b1, b2, b3, b4, b5, b6 being Element of c2 holds
( b1,b2 // b5,b6 & b3,b4 // b5,b6 implies b1,b2 // b3,b4 ) ) & ( for b1, b2, b3 being Element of c2 holds
ex b4 being Element of c2 st b1,b2 // b3,b4 ) & ( for b1, b2, b3, b4, b5, b6 being Element of c2 holds
( b1,b2 // b4,b5 & b1,b3 // b4,b6 implies b2,b3 // b5,b6 ) ) & ( for b1, b2 being Element of c2 holds
ex b3 being Element of c2 st b1,b3 // b3,b2 ) & ( for b1, b2, b3, b4 being Element of c2 holds
( b1,b2 // b3,b4 implies b1,b3 // b2,b4 ) ) ) by TDGROUP:21;
then c2 is WeakAffVect-like by Def1;
hence ex b1 being non empty AffinStruct st
( b1 is strict & not b1 is trivial & b1 is WeakAffVect-like ) ;
end;
end;

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

registration
cluster non empty AffVect-like -> non empty WeakAffVect-like AffinStruct ;
coherence
for b1 being non empty AffinStruct holds
( b1 is AffVect-like implies b1 is WeakAffVect-like )
proof
let c1 be non empty AffinStruct ;
assume E2: c1 is AffVect-like ;
c1 is WeakAffVect-like
proof
( ( for b1, b2, b3 being Element of c1 holds
( b1,b2 // b3,b3 implies b1 = b2 ) ) & ( for b1, b2, b3, b4, b5, b6 being Element of c1 holds
( b1,b2 // b5,b6 & b3,b4 // b5,b6 implies b1,b2 // b3,b4 ) ) & ( for b1, b2, b3 being Element of c1 holds
ex b4 being Element of c1 st b1,b2 // b3,b4 ) & ( for b1, b2, b3, b4, b5, b6 being Element of c1 holds
( b1,b2 // b4,b5 & b1,b3 // b4,b6 implies b2,b3 // b5,b6 ) ) & ( for b1, b2 being Element of c1 holds
ex b3 being Element of c1 st b1,b3 // b3,b2 ) & ( for b1, b2, b3, b4 being Element of c1 holds
( b1,b2 // b3,b4 implies b1,b3 // b2,b4 ) ) ) by E2, TDGROUP:def 8;
hence c1 is WeakAffVect-like by Def1;
end;
hence c1 is WeakAffVect-like ;
end;
end;

theorem Th1: :: AFVECT0:1
canceled;

theorem Th2: :: AFVECT0:2
for b1 being WeakAffVect
for b2, b3 being Element of b1 holds b2,b3 // b2,b3
proof
let c1 be WeakAffVect;
let c2, c3 be Element of c1;
ex b1 being Element of c1 st c2,c3 // c3,b1 by Def1;
hence c2,c3 // c2,c3 by Def1;
end;

theorem Th3: :: AFVECT0:3
for b1 being WeakAffVect
for b2 being Element of b1 holds b2,b2 // b2,b2 by Th2;

theorem Th4: :: AFVECT0:4
for b1 being WeakAffVect
for b2, b3, b4, b5 being Element of b1 holds
( b2,b3 // b4,b5 implies b4,b5 // b2,b3 )
proof
let c1 be WeakAffVect;
let c2, c3, c4, c5 be Element of c1;
assume E4: c2,c3 // c4,c5 ;
c4,c5 // c4,c5 by Th2;
hence c4,c5 // c2,c3 by E4, Def1;
end;

theorem Th5: :: AFVECT0:5
for b1 being WeakAffVect
for b2, b3, b4 being Element of b1 holds
( b2,b3 // b2,b4 implies b3 = b4 )
proof
let c1 be WeakAffVect;
let c2, c3, c4 be Element of c1;
assume c2,c3 // c2,c4 ;
then c2,c2 // c3,c4 by Def1;
then c3,c4 // c2,c2 by Th4;
hence c3 = c4 by Def1;
end;

theorem Th6: :: AFVECT0:6
for b1 being WeakAffVect
for b2, b3, b4, b5, b6 being Element of b1 holds
( b2,b3 // b4,b5 & b2,b3 // b4,b6 implies b5 = b6 )
proof
let c1 be WeakAffVect;
let c2, c3, c4, c5, c6 be Element of c1;
assume ( c2,c3 // c4,c5 & c2,c3 // c4,c6 ) ;
then ( c4,c5 // c2,c3 & c4,c6 // c2,c3 ) by Th4;
then c4,c5 // c4,c6 by Def1;
hence c5 = c6 by Th5;
end;

theorem Th7: :: AFVECT0:7
for b1 being WeakAffVect
for b2, b3 being Element of b1 holds b2,b2 // b3,b3
proof
let c1 be WeakAffVect;
let c2, c3 be Element of c1;
consider c4 being Element of c1 such that
E7: c2,c2 // c3,c4 by Def1;
c3,c4 // c2,c2 by E7, Th4;
hence c2,c2 // c3,c3 by E7, Def1;
end;

theorem Th8: :: AFVECT0:8
for b1 being WeakAffVect
for b2, b3, b4, b5 being Element of b1 holds
( b2,b3 // b4,b5 implies b3,b2 // b5,b4 )
proof
let c1 be WeakAffVect;
let c2, c3, c4, c5 be Element of c1;
assume E8: c2,c3 // c4,c5 ;
c2,c2 // c4,c4 by Th7;
hence c3,c2 // c5,c4 by E8, Def1;
end;

theorem Th9: :: AFVECT0:9
for b1 being WeakAffVect
for b2, b3, b4, b5, b6 being Element of b1 holds
( b2,b3 // b4,b5 & b2,b4 // b6,b5 implies b3 = b6 )
proof
let c1 be WeakAffVect;
let c2, c3, c4, c5, c6 be Element of c1;
assume E8: ( c2,c3 // c4,c5 & c2,c4 // c6,c5 ) ;
then c2,c4 // c3,c5 by Def1;
then c3,c5 // c2,c4 by Th4;
then E9: c5,c3 // c4,c2 by Th8;
c6,c5 // c2,c4 by E8, Th4;
then c5,c6 // c4,c2 by Th8;
then c5,c3 // c5,c6 by E9, Def1;
hence c3 = c6 by Th5;
end;

theorem Th10: :: AFVECT0:10
for b1 being WeakAffVect
for b2, b3, b4, b5, b6, b7, b8 being Element of b1 holds
( b2,b3 // b4,b5 & b6,b7 // b2,b3 & b6,b8 // b4,b5 implies b7 = b8 )
proof
let c1 be WeakAffVect;
let c2, c3, c4, c5, c6, c7, c8 be Element of c1;
assume E8: ( c2,c3 // c4,c5 & c6,c7 // c2,c3 & c6,c8 // c4,c5 ) ;
then c4,c5 // c2,c3 by Th4;
then c6,c7 // c4,c5 by E8, Def1;
then c6,c7 // c6,c8 by E8, Def1;
hence c7 = c8 by Th5;
end;

theorem Th11: :: AFVECT0:11
for b1 being WeakAffVect
for b2, b3, b4, b5, b6, b7, b8 being Element of b1 holds
( b2,b3 // b4,b5 & b6,b7 // b3,b2 & b6,b8 // b5,b4 implies b7 = b8 )
proof
let c1 be WeakAffVect;
let c2, c3, c4, c5, c6, c7, c8 be Element of c1;
assume E8: ( c2,c3 // c4,c5 & c6,c7 // c3,c2 & c6,c8 // c5,c4 ) ;
then c4,c5 // c2,c3 by Th4;
then c5,c4 // c3,c2 by Th8;
then c6,c7 // c5,c4 by E8, Def1;
then c6,c7 // c6,c8 by E8, Def1;
hence c7 = c8 by Th5;
end;

theorem Th12: :: AFVECT0:12
for b1 being WeakAffVect
for b2, b3, b4, b5, b6, b7, b8, b9, b10, b11 being Element of b1 holds
( b2,b3 // b4,b5 & b6,b7 // b8,b9 & b3,b10 // b6,b7 & b5,b11 // b8,b9 implies b2,b10 // b4,b11 )
proof
let c1 be WeakAffVect;
let c2, c3, c4, c5, c6, c7, c8, c9, c10, c11 be Element of c1;
assume E8: ( c2,c3 // c4,c5 & c6,c7 // c8,c9 & c3,c10 // c6,c7 & c5,c11 // c8,c9 ) ;
then c5,c11 // c6,c7 by Def1;
then E9: c3,c10 // c5,c11 by E8, Def1;
c3,c2 // c5,c4 by E8, Th8;
hence c2,c10 // c4,c11 by E9, Def1;
end;

theorem Th13: :: AFVECT0:13
for b1 being WeakAffVect
for b2, b3, b4, b5, b6, b7 being Element of b1 holds
( b2,b3 // b4,b5 & b2,b6 // b7,b5 implies b3,b6 // b7,b4 )
proof
let c1 be WeakAffVect;
let c2, c3, c4, c5, c6, c7 be Element of c1;
assume E9: ( c2,c3 // c4,c5 & c2,c6 // c7,c5 ) ;
consider c8 being Element of c1 such that
E10: c7,c5 // c4,c8 by Def1;
E11: c7,c4 // c5,c8 by E10, Def1;
c4,c8 // c7,c5 by E10, Th4;
then c2,c6 // c4,c8 by E9, Def1;
then c3,c6 // c5,c8 by E9, Def1;
hence c3,c6 // c7,c4 by E11, Def1;
end;

definition
let c1 be WeakAffVect;
let c2, c3 be Element of c1;
pred MDist c2,c3 means :Def2: :: AFVECT0:def 2
( a2,a3 // a3,a2 & a2 <> a3 );
irreflexivity
for b1 being Element of c1 holds
not ( b1,b1 // b1,b1 & b1 <> b1 ) ;
symmetry
for b1, b2 being Element of c1 holds
( b1,b2 // b2,b1 & b1 <> b2 implies ( b2,b1 // b1,b2 & b2 <> b1 ) ) by Th4;
end;

:: deftheorem Def2 defines MDist AFVECT0:def 2 :
for b1 being WeakAffVect
for b2, b3 being Element of b1 holds
( MDist b2,b3 iff ( b2,b3 // b3,b2 & b2 <> b3 ) );

theorem Th14: :: AFVECT0:14
canceled;

theorem Th15: :: AFVECT0:15
canceled;

theorem Th16: :: AFVECT0:16
for b1 being WeakAffVect holds
ex b2, b3 being Element of b1 st
( b2 <> b3 & not MDist b2,b3 )
proof
let c1 be WeakAffVect;
consider c2, c3 being Element of c1 such that
E10: c2 <> c3 by REALSET2:def 7;
now
consider c4 being Element of c1 such that
E11: c2,c4 // c4,c3 by Def1;
E12: now
assume E13: c2 = c4 ;
then c4,c3 // c2,c2 by E11, Th4;
hence ex b1, b2 being Element of c1 st
( b1 <> b2 & not MDist b1,b2 ) by E10, E13, Def1;
end;
now
assume E13: c2 <> c4 ;
now
assume E14: MDist c2,c4 ;
c4,c3 // c2,c4 by E11, Th4;
then E15: c3,c4 // c4,c2 by Th8;
c2,c4 // c4,c2 by E14, Def2;
then c2,c4 // c3,c4 by E15, Def1;
then c4,c2 // c4,c3 by Th8;
hence ex b1, b2 being Element of c1 st
( b1 <> b2 & not MDist b1,b2 ) by E10, Th5;
end;
hence ex b1, b2 being Element of c1 st
( b1 <> b2 & not MDist b1,b2 ) by E13;
end;
hence ex b1, b2 being Element of c1 st
( b1 <> b2 & not MDist b1,b2 ) by E12;
end;
hence ex b1, b2 being Element of c1 st
( b1 <> b2 & not MDist b1,b2 ) ;
end;

theorem Th17: :: AFVECT0:17
canceled;

theorem Th18: :: AFVECT0:18
for b1 being WeakAffVect
for b2, b3, b4 being Element of b1 holds
not ( MDist b2,b3 & MDist b2,b4 & not b3 = b4 & not MDist b3,b4 )
proof
let c1 be WeakAffVect;
let c2, c3, c4 be Element of c1;
assume E10: ( MDist c2,c3 & MDist c2,c4 ) ;
consider c5 being Element of c1 such that
E11: c4,c2 // c3,c5 by Def1;
E12: c3,c5 // c4,c2 by E11, Th4;
E13: ( c2,c3 // c3,c2 & c2,c4 // c4,c2 ) by E10, Def2;
then E14: c2,c4 // c3,c5 by E12, Def1;
E15: c4,c3 // c2,c5 by E11, Def1;
c3,c4 // c2,c5 by E13, E14, Def1;
then c3,c4 // c4,c3 by E15, Def1;
hence not ( not c3 = c4 & not MDist c3,c4 ) by Def2;
end;

theorem Th19: :: AFVECT0:19
for b1 being WeakAffVect
for b2, b3, b4, b5 being Element of b1 holds
( MDist b2,b3 & b2,b3 // b4,b5 implies MDist b4,b5 )
proof
let c1 be WeakAffVect;
let c2, c3, c4, c5 be Element of c1;
assume E10: ( MDist c2,c3 & c2,c3 // c4,c5 ) ;
then E11: ( c2 <> c3 & c2,c3 // c3,c2 ) by Def2;
E12: c4,c5 // c2,c3 by E10, Th4;
then c5,c4 // c3,c2 by Th8;
then c5,c4 // c2,c3 by E11, Def1;
then c4,c5 // c5,c4 by E12, Def1;
then ( c4 <> c5 implies MDist c4,c5 ) by Def2;
hence MDist c4,c5 by E10, Def1;
end;

definition
let c1 be WeakAffVect;
let c2, c3, c4 be Element of c1;
pred Mid c2,c3,c4 means :Def3: :: AFVECT0:def 3
a2,a3 // a3,a4;
end;

:: deftheorem Def3 defines Mid AFVECT0:def 3 :
for b1 being WeakAffVect
for b2, b3, b4 being Element of b1 holds
( Mid b2,b3,b4 iff b2,b3 // b3,b4 );

theorem Th20: :: AFVECT0:20
canceled;

theorem Th21: :: AFVECT0:21
for b1 being WeakAffVect
for b2, b3, b4 being Element of b1 holds
( Mid b2,b3,b4 implies Mid b4,b3,b2 )
proof
let c1 be WeakAffVect;
let c2, c3, c4 be Element of c1;
assume Mid c2,c3,c4 ;
then c2,c3 // c3,c4 by Def3;
then c3,c2 // c4,c3 by Th8;
then c4,c3 // c3,c2 by Th4;
hence Mid c4,c3,c2 by Def3;
end;

theorem Th22: :: AFVECT0:22
for b1 being WeakAffVect
for b2, b3 being Element of b1 holds
( Mid b2,b3,b3 iff b2 = b3 )
proof
let c1 be WeakAffVect;
let c2, c3 be Element of c1;
E12: now
assume Mid c2,c3,c3 ;
then c2,c3 // c3,c3 by Def3;
hence c2 = c3 by Def1;
end;
now
assume c2 = c3 ;
then c2,c3 // c3,c3 by Th7;
hence Mid c2,c3,c3 by Def3;
end;
hence ( Mid c2,c3,c3 iff c2 = c3 ) by E12;
end;

theorem Th23: :: AFVECT0:23
for b1 being WeakAffVect
for b2, b3 being Element of b1 holds
( Mid b2,b3,b2 iff ( b2 = b3 or MDist b2,b3 ) )
proof
let c1 be WeakAffVect;
let c2, c3 be Element of c1;
E13: now
assume Mid c2,c3,c2 ;
then c2,c3 // c3,c2 by Def3;
hence ( c2 = c3 or MDist c2,c3 ) by Def2;
end;
E14: now
assume c2 = c3 ;
then c2,c3 // c3,c2 by Th7;
hence Mid c2,c3,c2 by Def3;
end;
now
assume MDist c2,c3 ;
then c2,c3 // c3,c2 by Def2;
hence Mid c2,c3,c2 by Def3;
end;
hence ( Mid c2,c3,c2 iff ( c2 = c3 or MDist c2,c3 ) ) by E13, E14;
end;

theorem Th24: :: AFVECT0:24
for b1 being WeakAffVect
for b2, b3 being Element of b1 holds
ex b4 being Element of b1 st Mid b2,b4,b3
proof
let c1 be WeakAffVect;
let c2, c3 be Element of c1;
consider c4 being Element of c1 such that
E14: c2,c4 // c4,c3 by Def1;
Mid c2,c4,c3 by E14, Def3;
hence ex b1 being Element of c1 st Mid c2,b1,c3 ;
end;

theorem Th25: :: AFVECT0:25
for b1 being WeakAffVect
for b2, b3, b4, b5 being Element of b1 holds
not ( Mid b2,b3,b4 & Mid b2,b5,b4 & not b3 = b5 & not MDist b3,b5 )
proof
let c1 be WeakAffVect;
let c2, c3, c4, c5 be Element of c1;
assume ( Mid c2,c3,c4 & Mid c2,c5,c4 ) ;
then E15: ( c2,c3 // c3,c4 & c2,c5 // c5,c4 ) by Def3;
consider c6 being Element of c1 such that
E16: c5,c4 // c3,c6 by Def1;
E17: c3,c6 // c5,c4 by E16, Th4;
then c2,c5 // c3,c6 by E15, Def1;
then E18: c3,c5 // c4,c6 by E15, Def1;
c3,c5 // c6,c4 by E17, Def1;
then c5,c3 // c4,c6 by Th8;
then c3,c5 // c5,c3 by E18, Def1;
hence not ( not c3 = c5 & not MDist c3,c5 ) by Def2;
end;

theorem Th26: :: AFVECT0:26
for b1 being WeakAffVect
for b2, b3 being Element of b1 holds
ex b4 being Element of b1 st Mid b2,b3,b4
proof
let c1 be WeakAffVect;
let c2, c3 be Element of c1;
consider c4 being Element of c1 such that
E16: c2,c3 // c3,c4 by Def1;
Mid c2,c3,c4 by E16, Def3;
hence ex b1 being Element of c1 st Mid c2,c3,b1 ;
end;

theorem Th27: :: AFVECT0:27
for b1 being WeakAffVect
for b2, b3, b4, b5 being Element of b1 holds
( Mid b2,b3,b4 & Mid b2,b3,b5 implies b4 = b5 )
proof
let c1 be WeakAffVect;
let c2, c3, c4, c5 be Element of c1;
assume ( Mid c2,c3,c4 & Mid c2,c3,c5 ) ;
then ( c2,c3 // c3,c4 & c2,c3 // c3,c5 ) by Def3;
then ( c3,c4 // c2,c3 & c3,c5 // c2,c3 ) by Th4;
then c3,c4 // c3,c5 by Def1;
hence c4 = c5 by Th5;
end;

theorem Th28: :: AFVECT0:28
for b1 being WeakAffVect
for b2, b3, b4, b5 being Element of b1 holds
( Mid b2,b3,b4 & MDist b3,b5 implies Mid b2,b5,b4 )
proof
let c1 be WeakAffVect;
let c2, c3, c4, c5 be Element of c1;
assume ( Mid c2,c3,c4 & MDist c3,c5 ) ;
then E18: ( c2,c3 // c3,c4 & c3,c5 // c5,c3 ) by Def2, Def3;
consider c6 being Element of c1 such that
E19: c5,c3 // c4,c6 by Def1;
c4,c6 // c5,c3 by E19, Th4;
then E20: c3,c5 // c4,c6 by E18, Def1;
c3,c2 // c4,c3 by E18, Th8;
then E21: c2,c5 // c3,c6 by E20, Def1;
c5,c4 // c3,c6 by E19, Def1;
then c2,c5 // c5,c4 by E21, Def1;
hence Mid c2,c5,c4 by Def3;
end;

theorem Th29: :: AFVECT0:29
for b1 being WeakAffVect
for b2, b3, b4, b5, b6 being Element of b1 holds
( Mid b2,b3,b4 & Mid b2,b5,b6 & MDist b3,b5 implies b4 = b6 )
proof
let c1 be WeakAffVect;
let c2, c3, c4, c5, c6 be Element of c1;
assume E19: ( Mid c2,c3,c4 & Mid c2,c5,c6 & MDist c3,c5 ) ;
then Mid c2,c5,c4 by Th28;
hence c4 = c6 by E19, Th27;
end;

theorem Th30: :: AFVECT0:30
for b1 being WeakAffVect
for b2, b3, b4, b5, b6 being Element of b1 holds
( Mid b2,b3,b4 & Mid b5,b3,b6 implies b2,b5 // b6,b4 )
proof
let c1 be WeakAffVect;
let c2, c3, c4, c5, c6 be Element of c1;
assume E20: ( Mid c2,c3,c4 & Mid c5,c3,c6 ) ;
consider c7 being Element of c1 such that
E21: c6,c3 // c4,c7 by Def1;
E22: c4,c7 // c6,c3 by E21, Th4;
c5,c3 // c3,c6 by E20, Def3;
then c3,c5 // c6,c3 by Th8;
then E23: c3,c5 // c4,c7 by E22, Def1;
c2,c3 // c3,c4 by E20, Def3;
then c3,c2 // c4,c3 by Th8;
then E24: c2,c5 // c3,c7 by E23, Def1;
c6,c4 // c3,c7 by E21, Def1;
hence c2,c5 // c6,c4 by E24, Def1;
end;

theorem Th31: :: AFVECT0:31
for b1 being WeakAffVect
for b2, b3, b4, b5, b6, b7 being Element of b1 holds
( Mid b2,b3,b4 & Mid b5,b6,b7 & MDist b3,b6 implies b2,b5 // b7,b4 )
proof
let c1 be WeakAffVect;
let c2, c3, c4, c5, c6, c7 be Element of c1;
assume E20: ( Mid c2,c3,c4 & Mid c5,c6,c7 & MDist c3,c6 ) ;
then Mid c2,c6,c4 by Th28;
hence c2,c5 // c7,c4 by E20, Th30;
end;

definition
let c1 be WeakAffVect;
let c2, c3 be Element of c1;
func PSym c2,c3 -> Element of a1 means :Def4: :: AFVECT0:def 4
 Mid a3,a2,a4;
correctness
existence
ex b1 being Element of c1 st Mid c3,c2,b1;
uniqueness
for b1, b2 being Element of c1 holds
( Mid c3,c2,b1 & Mid c3,c2,b2 implies b1 = b2 );
by Th26, Th27;
end;

:: deftheorem Def4 defines PSym AFVECT0:def 4 :
for b1 being WeakAffVect
for b2, b3, b4 being Element of b1 holds
( b4 = PSym b2,b3 iff Mid b3,b2,b4 );

theorem Th32: :: AFVECT0:32
canceled;

theorem Th33: :: AFVECT0:33
for b1 being WeakAffVect
for b2, b3, b4 being Element of b1 holds
( PSym b2,b3 = b4 iff b3,b2 // b2,b4 )
proof
let c1 be WeakAffVect;
let c2, c3, c4 be Element of c1;
E21: now
assume PSym c2,c3 = c4 ;
then Mid c3,c2,c4 by Def4;
hence c3,c2 // c2,c4 by Def3;
end;
now
assume c3,c2 // c2,c4 ;
then Mid c3,c2,c4 by Def3;
hence PSym c2,c3 = c4 by Def4;
end;
hence ( PSym c2,c3 = c4 iff c3,c2 // c2,c4 ) by E21;
end;

theorem Th34: :: AFVECT0:34
canceled;

theorem Th35: :: AFVECT0:35
for b1 being WeakAffVect
for b2, b3 being Element of b1 holds
( PSym b2,b3 = b3 iff ( b3 = b2 or MDist b3,b2 ) )
proof
let c1 be WeakAffVect;
let c2, c3 be Element of c1;
E22: now
assume PSym c2,c3 = c3 ;
then Mid c3,c2,c3 by Def4;
hence ( c3 = c2 or MDist c3,c2 ) by Th23;
end;
now
assume ( c3 = c2 or MDist c3,c2 ) ;
then Mid c3,c2,c3 by Th23;
hence PSym c2,c3 = c3 by Def4;
end;
hence ( PSym c2,c3 = c3 iff ( c3 = c2 or MDist c3,c2 ) ) by E22;
end;

theorem Th36: :: AFVECT0:36
for b1 being WeakAffVect
for b2, b3 being Element of b1 holds PSym b2,(PSym b2,b3) = b3
proof
let c1 be WeakAffVect;
let c2, c3 be Element of c1;
Mid c3,c2, PSym c2,c3 by Def4;
then Mid PSym c2,c3,c2,c3 by Th21;
hence PSym c2,(PSym c2,c3) = c3 by Def4;
end;

theorem Th37: :: AFVECT0:37
for b1 being WeakAffVect
for b2, b3, b4 being Element of b1 holds
( PSym b2,b3 = PSym b2,b4 implies b3 = b4 )
proof
let c1 be WeakAffVect;
let c2, c3, c4 be Element of c1;
assume E24: PSym c2,c3 = PSym c2,c4 ;
( PSym c2,(PSym c2,c3) = c3 & PSym c2,(PSym c2,c4) = c4 ) by Th36;
hence c3 = c4 by E24;
end;

theorem Th38: :: AFVECT0:38
for b1 being WeakAffVect
for b2, b3 being Element of b1 holds
ex b4 being Element of b1 st PSym b2,b4 = b3
proof
let c1 be WeakAffVect;
let c2, c3 be Element of c1;
PSym c2,(PSym c2,c3) = c3 by Th36;
hence ex b1 being Element of c1 st PSym c2,b1 = c3 ;
end;

theorem Th39: :: AFVECT0:39
for b1 being WeakAffVect
for b2, b3, b4 being Element of b1 holds b2,b3 // PSym b4,b3, PSym b4,b2
proof
let c1 be WeakAffVect;
let c2, c3, c4 be Element of c1;
( Mid c2,c4, PSym c4,c2 & Mid c3,c4, PSym c4,c3 ) by Def4;
hence c2,c3 // PSym c4,c3, PSym c4,c2 by Th30;
end;

theorem Th40: :: AFVECT0:40
for b1 being WeakAffVect
for b2, b3, b4, b5, b6 being Element of b1 holds
( b2,b3 // b4,b5 iff PSym b6,b2, PSym b6,b3 // PSym b6,b4, PSym b6,b5 )
proof
let c1 be WeakAffVect;
let c2, c3, c4, c5, c6 be Element of c1;
E26: now
assume E27: c2,c3 // c4,c5 ;
E28: ( c2,c3 // PSym c6,c3, PSym c6,c2 & c4,c5 // PSym c6,c5, PSym c6,c4 ) by Th39;
then PSym c6,c5, PSym c6,c4 // c4,c5 by Th4;
then E29: PSym c6,c5, PSym c6,c4 // c2,c3 by E27, Def1;
PSym c6,c3, PSym c6,c2 // c2,c3 by E28, Th4;
then PSym c6,c3, PSym c6,c2 // PSym c6,c5, PSym c6,c4 by E29, Def1;
hence PSym c6,c2, PSym c6,c3 // PSym c6,c4, PSym c6,c5 by Th8;
end;
now
assume E27: PSym c6,c2, PSym c6,c3 // PSym c6,c4, PSym c6,c5 ;
E28: ( c2,c3 // PSym c6,c3, PSym c6,c2 & c4,c5 // PSym c6,c5, PSym c6,c4 ) by Th39;
c5,c4 // PSym c6,c4, PSym c6,c5 by Th39;
then c5,c4 // PSym c6,c2, PSym c6,c3 by E27, Def1;
then c4,c5 // PSym c6,c3, PSym c6,c2 by Th8;
hence c2,c3 // c4,c5 by E28, Def1;
end;
hence ( c2,c3 // c4,c5 iff PSym c6,c2, PSym c6,c3 // PSym c6,c4, PSym c6,c5 ) by E26;
end;

theorem Th41: :: AFVECT0:41
for b1 being WeakAffVect
for b2, b3, b4 being Element of b1 holds
( MDist b2,b3 iff MDist PSym b4,b2, PSym b4,b3 )
proof
let c1 be WeakAffVect;
let c2, c3, c4 be Element of c1;
E26: now
assume MDist c2,c3 ;
then ( c2,c3 // c3,c2 & c2 <> c3 ) by Def2;
then ( PSym c4,c2, PSym c4,c3 // PSym c4,c3, PSym c4,c2 & PSym c4,c2 <> PSym c4,c3 ) by Th37, Th40;
hence MDist PSym c4,c2, PSym c4,c3 by Def2;
end;
now
assume MDist PSym c4,c2, PSym c4,c3 ;
then ( PSym c4,c2, PSym c4,c3 // PSym c4,c3, PSym c4,c2 & PSym c4,c2 <> PSym c4,c3 ) by Def2;
then ( c2,c3 // c3,c2 & c2 <> c3 ) by Th40;
hence MDist c2,c3 by Def2;
end;
hence ( MDist c2,c3 iff MDist PSym c4,c2, PSym c4,c3 ) by E26;
end;

theorem Th42: :: AFVECT0:42
for b1 being WeakAffVect
for b2, b3, b4, b5 being Element of b1 holds
( Mid b2,b3,b4 iff Mid PSym b5,b2, PSym b5,b3, PSym b5,b4 )
proof
let c1 be WeakAffVect;
let c2, c3, c4, c5 be Element of c1;
E27: now
assume Mid c2,c3,c4 ;
then c2,c3 // c3,c4 by Def3;
then PSym c5,c2, PSym c5,c3 // PSym c5,c3, PSym c5,c4 by Th40;
hence Mid PSym c5,c2, PSym c5,c3, PSym c5,c4 by Def3;
end;
now
assume Mid PSym c5,c2, PSym c5,c3, PSym c5,c4 ;
then PSym c5,c2, PSym c5,c3 // PSym c5,c3, PSym c5,c4 by Def3;
then c2,c3 // c3,c4 by Th40;
hence Mid c2,c3,c4 by Def3;
end;
hence ( Mid c2,c3,c4 iff Mid PSym c5,c2, PSym c5,c3, PSym c5,c4 ) by E27;
end;

theorem Th43: :: AFVECT0:43
for b1 being WeakAffVect
for b2, b3, b4 being Element of b1 holds
( PSym b2,b3 = PSym b4,b3 iff ( b2 = b4 or MDist b2,b4 ) )
proof
let c1 be WeakAffVect;
let c2, c3, c4 be Element of c1;
E28: now
assume E29: PSym c2,c3 = PSym c4,c3 ;
( Mid c3,c2, PSym c2,c3 & Mid c3,c4, PSym c4,c3 ) by Def4;
hence ( c2 = c4 or MDist c2,c4 ) by E29, Th25;
end;
now
assume E29: MDist c2,c4 ;
( Mid c3,c2, PSym c2,c3 & Mid c3,c4, PSym c4,c3 ) by Def4;
hence PSym c2,c3 = PSym c4,c3 by E29, Th29;
end;
hence ( PSym c2,c3 = PSym c4,c3 iff ( c2 = c4 or MDist c2,c4 ) ) by E28;
end;

theorem Th44: :: AFVECT0:44
for b1 being WeakAffVect
for b2, b3, b4 being Element of b1 holds PSym b2,(PSym b3,(PSym b2,b4)) = PSym (PSym b2,b3),b4
proof
let c1 be WeakAffVect;
let c2, c3, c4 be Element of c1;
Mid PSym c2,c4,c3, PSym c3,(PSym c2,c4) by Def4;
then Mid PSym c2,(PSym c2,c4), PSym c2,c3, PSym c2,(PSym c3,(PSym c2,c4)) by Th42;
then PSym c2,(PSym c3,(PSym c2,c4)) = PSym (PSym c2,c3),(PSym c2,(PSym c2,c4)) by Def4;
hence PSym c2,(PSym c3,(PSym c2,c4)) = PSym (PSym c2,c3),c4 by Th36;
end;

theorem Th45: :: AFVECT0:45
for b1 being WeakAffVect
for b2, b3, b4 being Element of b1 holds
( PSym b2,(PSym b3,b4) = PSym b3,(PSym b2,b4) iff not ( not b2 = b3 & not MDist b2,b3 & not MDist b3, PSym b2,b3 ) )
proof
let c1 be WeakAffVect;
let c2, c3, c4 be Element of c1;
E29: now
assume PSym c2,(PSym c3,c4) = PSym c3,(PSym c2,c4) ;
then PSym c2,(PSym c3,(PSym c2,c4)) = PSym c3,c4 by Th36;
then PSym (PSym c2,c3),c4 = PSym c3,c4 by Th44;
then ( c3 = PSym c2,c3 or MDist c3, PSym c2,c3 ) by Th43;
then E30: ( Mid c3,c2,c3 or MDist c3, PSym c2,c3 ) by Def4;
hence not ( not c2 = c3 & not MDist c3,c2 & not MDist c3, PSym c2,c3 ) by Th23;
thus not ( not c2 = c3 & not MDist c2,c3 & not MDist c3, PSym c2,c3 ) by E30, Th23;
end;
now
assume not ( not c2 = c3 & not MDist c2,c3 & not MDist c3, PSym c2,c3 ) ;
then ( Mid c3,c2,c3 or MDist c3, PSym c2,c3 ) by Th23;
then PSym (PSym c2,c3),c4 = PSym c3,c4 by Def4, Th43;
then PSym c2,(PSym c3,(PSym c2,c4)) = PSym c3,c4 by Th44;
hence PSym c2,(PSym c3,c4) = PSym c3,(PSym c2,c4) by Th36;
end;
hence ( PSym c2,(PSym c3,c4) = PSym c3,(PSym c2,c4) iff not ( not c2 = c3 & not MDist c2,c3 & not MDist c3, PSym c2,c3 ) ) by E29;
end;

theorem Th46: :: AFVECT0:46
for b1 being WeakAffVect
for b2, b3, b4, b5 being Element of b1 holds PSym b2,(PSym b3,(PSym b4,b5)) = PSym b4,(PSym b3,(