:: AFF_1 semantic presentation

definition
let c1 be AffinSpace;
let c2, c3, c4 be Element of c1;
pred LIN c2,c3,c4 means :Def1: :: AFF_1:def 1
a2,a3 // a2,a4;
end;

:: deftheorem Def1 defines LIN AFF_1:def 1 :
for b1 being AffinSpace
for b2, b3, b4 being Element of b1 holds
( LIN b2,b3,b4 iff b2,b3 // b2,b4 );

theorem Th1: :: AFF_1:1
canceled;

theorem Th2: :: AFF_1:2
canceled;

theorem Th3: :: AFF_1:3
canceled;

theorem Th4: :: AFF_1:4
canceled;

theorem Th5: :: AFF_1:5
canceled;

theorem Th6: :: AFF_1:6
canceled;

theorem Th7: :: AFF_1:7
canceled;

theorem Th8: :: AFF_1:8
canceled;

theorem Th9: :: AFF_1:9
canceled;

theorem Th10: :: AFF_1:10
for b1 being AffinSpace
for b2 being Element of b1 holds
not for b3 being Element of b1 holds not b2 <> b3
proof
let c1 be AffinSpace;
let c2 be Element of c1;
consider c3, c4 being Element of c1 such that
E3: c3 <> c4 by DIRAF:47;
not ( c2 = c3 & not c2 <> c4 ) by E3;
hence not for b1 being Element of c1 holds not c2 <> b1 ;
end;

theorem Th11: :: AFF_1:11
for b1 being AffinSpace
for b2, b3 being Element of b1 holds
( b2,b3 // b3,b2 & b2,b3 // b2,b3 )
proof
let c1 be AffinSpace;
let c2, c3 be Element of c1;
thus c2,c3 // c3,c2 by DIRAF:47;
c3,c2 // c3,c3 by DIRAF:47;
hence c2,c3 // c2,c3 by DIRAF:47;
end;

Lemma4: for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1 holds
( b2,b3 // b4,b5 implies b4,b5 // b2,b3 )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5 be Element of c1;
assume E5: c2,c3 // c4,c5 ;
now
assume c2 <> c3 ;
then ( c2 <> c3 & c2,c3 // c2,c3 ) by Th11;
hence c4,c5 // c2,c3 by E5, DIRAF:47;
end;
hence c4,c5 // c2,c3 by DIRAF:47;
end;

theorem Th12: :: AFF_1:12
for b1 being AffinSpace
for b2, b3, b4 being Element of b1 holds
( b2,b3 // b4,b4 & b4,b4 // b2,b3 )
proof
let c1 be AffinSpace;
let c2, c3, c4 be Element of c1;
thus c2,c3 // c4,c4 by DIRAF:47;
hence c4,c4 // c2,c3 by Lemma4;
end;

Lemma6: for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1 holds
( b2,b3 // b4,b5 implies b3,b2 // b4,b5 )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5 be Element of c1;
assume c2,c3 // c4,c5 ;
then ( c2,c3 // c4,c5 & c2,c3 // c3,c2 ) by Th11;
then ( c3,c2 // c4,c5 or c2 = c3 ) by DIRAF:47;
hence c3,c2 // c4,c5 by Th12;
end;

Lemma7: for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1 holds
( b2,b3 // b4,b5 implies b2,b3 // b5,b4 )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5 be Element of c1;
assume c2,c3 // c4,c5 ;
then c4,c5 // c2,c3 by Lemma4;
then c5,c4 // c2,c3 by Lemma6;
hence c2,c3 // c5,c4 by Lemma4;
end;

theorem Th13: :: AFF_1:13
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1 holds
( b2,b3 // b4,b5 implies ( b2,b3 // b5,b4 & b3,b2 // b4,b5 & b3,b2 // b5,b4 & b4,b5 // b2,b3 & b4,b5 // b3,b2 & b5,b4 // b2,b3 & b5,b4 // b3,b2 ) )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5 be Element of c1;
assume E9: c2,c3 // c4,c5 ;
hence ( c2,c3 // c5,c4 & c3,c2 // c4,c5 ) by Lemma6, Lemma7;
hence c3,c2 // c5,c4 by Lemma6;
thus c4,c5 // c2,c3 by E9, Lemma4;
hence ( c4,c5 // c3,c2 & c5,c4 // c2,c3 ) by Lemma6, Lemma7;
hence c5,c4 // c3,c2 by Lemma7;
end;

theorem Th14: :: AFF_1:14
for b1 being AffinSpace
for b2, b3, b4, b5, b6, b7 being Element of b1 holds
( b2 <> b3 & not ( not ( b2,b3 // b4,b5 & b2,b3 // b6,b7 ) & not ( b2,b3 // b4,b5 & b6,b7 // b2,b3 ) & not ( b4,b5 // b2,b3 & b6,b7 // b2,b3 ) & not ( b4,b5 // b2,b3 & b2,b3 // b6,b7 ) ) implies b4,b5 // b6,b7 )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5, c6, c7 be Element of c1;
assume ( c2 <> c3 & not ( not ( c2,c3 // c4,c5 & c2,c3 // c6,c7 ) & not ( c2,c3 // c4,c5 & c6,c7 // c2,c3 ) & not ( c4,c5 // c2,c3 & c6,c7 // c2,c3 ) & not ( c4,c5 // c2,c3 & c2,c3 // c6,c7 ) ) ) ;
then ( c2 <> c3 & c2,c3 // c4,c5 & c2,c3 // c6,c7 ) by Th13;
hence c4,c5 // c6,c7 by DIRAF:47;
end;

Lemma10: for b1 being AffinSpace
for b2, b3, b4 being Element of b1 holds
( LIN b2,b3,b4 implies ( LIN b2,b4,b3 & LIN b3,b2,b4 ) )
proof
let c1 be AffinSpace;
let c2, c3, c4 be Element of c1;
assume LIN c2,c3,c4 ;
then c2,c3 // c2,c4 by Def1;
then ( c2,c4 // c2,c3 & c3,c2 // c3,c4 ) by Th13, DIRAF:47;
hence ( LIN c2,c4,c3 & LIN c3,c2,c4 ) by Def1;
end;

theorem Th15: :: AFF_1:15
for b1 being AffinSpace
for b2, b3, b4 being Element of b1 holds
( LIN b2,b3,b4 implies ( LIN b2,b4,b3 & LIN b3,b2,b4 & LIN b3,b4,b2 & LIN b4,b2,b3 & LIN b4,b3,b2 ) )
proof
let c1 be AffinSpace;
let c2, c3, c4 be Element of c1;
assume LIN c2,c3,c4 ;
hence ( LIN c2,c4,c3 & LIN c3,c2,c4 ) by Lemma10;
hence ( LIN c3,c4,c2 & LIN c4,c2,c3 ) by Lemma10;
hence LIN c4,c3,c2 by Lemma10;
end;

theorem Th16: :: AFF_1:16
for b1 being AffinSpace
for b2, b3 being Element of b1 holds
( LIN b2,b2,b3 & LIN b2,b3,b3 & LIN b2,b3,b2 )
proof
let c1 be AffinSpace;
let c2, c3 be Element of c1;
( c2,c2 // c2,c3 & c2,c3 // c2,c3 & c2,c3 // c2,c2 ) by Th11, Th12;
hence ( LIN c2,c2,c3 & LIN c2,c3,c3 & LIN c2,c3,c2 ) by Def1;
end;

theorem Th17: :: AFF_1:17
for b1 being AffinSpace
for b2, b3, b4, b5, b6 being Element of b1 holds
( b2 <> b3 & LIN b2,b3,b4 & LIN b2,b3,b5 & LIN b2,b3,b6 implies LIN b4,b5,b6 )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5, c6 be Element of c1;
assume E14: ( c2 <> c3 & LIN c2,c3,c4 & LIN c2,c3,c5 & LIN c2,c3,c6 ) ;
E15: now
assume c2 = c4 ;
then ( c4 <> c3 & c4,c3 // c4,c5 & c4,c3 // c4,c6 ) by E14, Def1;
then c4,c5 // c4,c6 by Th14;
hence LIN c4,c5,c6 by Def1;
end;
now
assume E16: c2 <> c4 ;
( c2,c3 // c2,c4 & c2,c3 // c2,c5 & c2,c3 // c2,c6 ) by E14, Def1;
then ( c2,c4 // c2,c5 & c2,c4 // c2,c6 ) by E14, Th14;
then ( c4,c2 // c4,c5 & c4,c2 // c4,c6 ) by DIRAF:47;
then c4,c5 // c4,c6 by E16, Th14;
hence LIN c4,c5,c6 by Def1;
end;
hence LIN c4,c5,c6 by E15;
end;

theorem Th18: :: AFF_1:18
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1 holds
( b2 <> b3 & LIN b2,b3,b4 & b2,b3 // b4,b5 implies LIN b2,b3,b5 )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5 be Element of c1;
assume E15: ( c2 <> c3 & LIN c2,c3,c4 & c2,c3 // c4,c5 ) ;
now
assume E16: c4 <> c2 ;
c2,c3 // c2,c4 by E15, Def1;
then c2,c4 // c4,c5 by E15, Th14;
then c4,c2 // c4,c5 by Th13;
then LIN c4,c2,c5 by Def1;
then ( LIN c2,c4,c5 & LIN c2,c4,c3 & LIN c2,c4,c2 ) by E15, Th15, Th16;
hence LIN c2,c3,c5 by E16, Th17;
end;
hence LIN c2,c3,c5 by E15, Def1;
end;

theorem Th19: :: AFF_1:19
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1 holds
( LIN b2,b3,b4 & LIN b2,b3,b5 implies b2,b3 // b4,b5 )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5 be Element of c1;
assume E16: ( LIN c2,c3,c4 & LIN c2,c3,c5 ) ;
now
assume E17: c2 <> c3 ;
now
E18: ( c2,c3 // c2,c4 & c2,c3 // c2,c5 ) by E16, Def1;
then c2,c4 // c2,c5 by E17, Th14;
then c4,c2 // c4,c5 by DIRAF:47;
then c2,c4 // c4,c5 by Th13;
hence c2,c3 // c4,c5 by E18, Th14;
end;
hence c2,c3 // c4,c5 ;
end;
hence c2,c3 // c4,c5 by Th12;
end;

theorem Th20: :: AFF_1:20
for b1 being AffinSpace
for b2, b3, b4, b5, b6 being Element of b1 holds
( b2 <> b3 & LIN b4,b5,b2 & LIN b4,b5,b3 & LIN b2,b3,b6 implies LIN b4,b5,b6 )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5, c6 be Element of c1;
assume E17: ( c2 <> c3 & LIN c4,c5,c2 & LIN c4,c5,c3 & LIN c2,c3,c6 ) ;
now
assume E18: c4 <> c5 ;
( LIN c4,c5,c5 & LIN c4,c5,c4 ) by Th16;
then ( LIN c3,c2,c5 & LIN c3,c2,c4 & LIN c3,c2,c6 ) by E17, E18, Th15, Th17;
hence LIN c4,c5,c6 by E17, Th17;
end;
hence LIN c4,c5,c6 by Th16;
end;

theorem Th21: :: AFF_1:21
for b1 being AffinSpace holds
not for b2, b3, b4 being Element of b1 holds LIN b2,b3,b4
proof
let c1 be AffinSpace;
consider c2, c3, c4 being Element of c1 such that
E18: not c2,c3 // c2,c4 by DIRAF:47;
not LIN c2,c3,c4 by E18, Def1;
hence not for b1, b2, b3 being Element of c1 holds LIN b1,b2,b3 ;
end;

theorem Th22: :: AFF_1:22
for b1 being AffinSpace
for b2, b3 being Element of b1 holds
not ( b2 <> b3 & ( for b4 being Element of b1 holds LIN b2,b3,b4 ) )
proof
let c1 be AffinSpace;
let c2, c3 be Element of c1;
assume E18: c2 <> c3 ;
assume E19: for b1 being Element of c1 holds LIN c2,c3,b1 ;
consider c4, c5, c6 being Element of c1 such that
E20: not LIN c4,c5,c6 by Th21;
( LIN c2,c3,c4 & LIN c2,c3,c5 & LIN c2,c3,c6 ) by E19;
hence not verum by E18, E20, Th17;
end;

theorem Th23: :: AFF_1:23
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1 holds
( not LIN b2,b3,b4 & LIN b2,b4,b5 & b3,b4 // b3,b5 implies b4 = b5 )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5 be Element of c1;
assume E18: ( not LIN c2,c3,c4 & LIN c2,c4,c5 & c3,c4 // c3,c5 ) ;
assume E19: c4 <> c5 ;
LIN c3,c4,c5 by E18, Def1;
then ( LIN c4,c5,c3 & LIN c4,c5,c2 & LIN c4,c5,c4 ) by E18, Th15, Th16;
hence not verum by E18, E19, Th17;
end;

definition
let c1 be AffinSpace;
let c2, c3 be Element of c1;
func Line c2,c3 -> Subset of a1 means :Def2: :: AFF_1:def 2
for b1 being Element of a1 holds
( b1 in a4 iff LIN a2,a3,b1 );
existence
ex b1 being Subset of c1 st
for b2 being Element of c1 holds
( b2 in b1 iff LIN c2,c3,b2 )
proof
defpred S1[ set ] means for b1 being Element of c1 holds
( b1 = a1 implies LIN c2,c3,b1 );
consider c4 being Subset of c1 such that
E18: for b1 being set holds
( b1 in c4 iff ( b1 in the carrier of c1 & S1[b1] ) ) from SUBSET_1:sch 1();
 take c4 ;
let c5 be Element of c1;
thus ( c5 in c4 implies LIN c2,c3,c5 ) by E18;
assume LIN c2,c3,c5 ;
then ( c5 in the carrier of c1 & ( for b1 being Element of c1 holds
( b1 = c5 implies LIN c2,c3,b1 ) ) ) ;
hence c5 in c4 by E18;
end;
uniqueness
for b1, b2 being Subset of c1 holds
( ( for b3 being Element of c1 holds
( b3 in b1 iff LIN c2,c3,b3 ) ) & ( for b3 being Element of c1 holds
( b3 in b2 iff LIN c2,c3,b3 ) ) implies b1 = b2 )
proof
let c4, c5 be Subset of c1;
assume that
E18: for b1 being Element of c1 holds
( b1 in c4 iff LIN c2,c3,b1 ) and
E19: for b1 being Element of c1 holds
( b1 in c5 iff LIN c2,c3,b1 ) ;
for b1 being set holds
( b1 in c4 iff b1 in c5 )
proof
let c6 be set ;
thus ( c6 in c4 implies c6 in c5 )
proof
assume E20: c6 in c4 ;
then reconsider c7 = c6 as Element of c1 ;
LIN c2,c3,c7 by E18, E20;
hence c6 in c5 by E19;
end;
assume E20: c6 in c5 ;
then reconsider c7 = c6 as Element of c1 ;
LIN c2,c3,c7 by E19, E20;
hence c6 in c4 by E18;
end;
hence c4 = c5 by TARSKI:2;
end;
end;

:: deftheorem Def2 defines Line AFF_1:def 2 :
for b1 being AffinSpace
for b2, b3 being Element of b1
for b4 being Subset of b1 holds
( b4 = Line b2,b3 iff for b5 being Element of b1 holds
( b5 in b4 iff LIN b2,b3,b5 ) );

Lemma19: for b1 being AffinSpace
for b2, b3 being Element of b1 holds Line b2,b3 c= Line b3,b2
proof
let c1 be AffinSpace;
let c2, c3 be Element of c1;
now
let c4 be set ;
assume E20: c4 in Line c2,c3 ;
then reconsider c5 = c4 as Element of c1 ;
LIN c2,c3,c5 by E20, Def2;
then LIN c3,c2,c5 by Th15;
hence c4 in Line c3,c2 by Def2;
end;
hence Line c2,c3 c= Line c3,c2 by TARSKI:def 3;
end;

theorem Th24: :: AFF_1:24
canceled;

theorem Th25: :: AFF_1:25
for b1 being AffinSpace
for b2, b3 being Element of b1 holds Line b2,b3 = Line b3,b2
proof
let c1 be AffinSpace;
let c2, c3 be Element of c1;
( Line c2,c3 c= Line c3,c2 & Line c3,c2 c= Line c2,c3 ) by Lemma19;
hence Line c2,c3 = Line c3,c2 by XBOOLE_0:def 10;
end;

definition
let c1 be AffinSpace;
let c2, c3 be Element of c1;
redefine func Line as Line c2,c3 -> Subset of a1;
commutativity
for b1, b2 being Element of c1 holds Line b1,b2 = Line b2,b1 by Th25;
end;

theorem Th26: :: AFF_1:26
for b1 being AffinSpace
for b2, b3 being Element of b1 holds
( b2 in Line b2,b3 & b3 in Line b2,b3 )
proof
let c1 be AffinSpace;
let c2, c3 be Element of c1;
( LIN c2,c3,c2 & LIN c2,c3,c3 ) by Th16;
hence ( c2 in Line c2,c3 & c3 in Line c2,c3 ) by Def2;
end;

theorem Th27: :: AFF_1:27
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1 holds
( b2 in Line b3,b4 & b5 in Line b3,b4 & b2 <> b5 implies Line b2,b5 c= Line b3,b4 )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5 be Element of c1;
assume E23: ( c2 in Line c3,c4 & c5 in Line c3,c4 & c2 <> c5 ) ;
then E24: ( LIN c3,c4,c2 & LIN c3,c4,c5 ) by Def2;
now
let c6 be set ;
assume E25: c6 in Line c2,c5 ;
then reconsider c7 = c6 as Element of c1 ;
LIN c2,c5,c7 by E25, Def2;
then LIN c3,c4,c7 by E23, E24, Th20;
hence c6 in Line c3,c4 by Def2;
end;
hence Line c2,c5 c= Line c3,c4 by TARSKI:def 3;
end;

theorem Th28: :: AFF_1:28
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1 holds
( b2 in Line b3,b4 & b5 in Line b3,b4 & b3 <> b4 implies Line b3,b4 c= Line b2,b5 )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5 be Element of c1;
assume E24: ( c2 in Line c3,c4 & c5 in Line c3,c4 & c3 <> c4 ) ;
then E25: ( LIN c3,c4,c2 & LIN c3,c4,c5 ) by Def2;
now
let c6 be set ;
assume E26: c6 in Line c3,c4 ;
then reconsider c7 = c6 as Element of c1 ;
LIN c3,c4,c7 by E26, Def2;
then LIN c2,c5,c7 by E24, E25, Th17;
hence c6 in Line c2,c5 by Def2;
end;
hence Line c3,c4 c= Line c2,c5 by TARSKI:def 3;
end;

definition
let c1 be AffinSpace;
let c2 be Subset of c1;
attr a2 is being_line means :Def3: :: AFF_1:def 3
ex b1, b2 being Element of a1 st
( b1 <> b2 & a2 = Line b1,b2 );
end;

:: deftheorem Def3 defines being_line AFF_1:def 3 :
for b1 being AffinSpace
for b2 being Subset of b1 holds
( b2 is being_line iff ex b3, b4 being Element of b1 st
( b3 <> b4 & b2 = Line b3,b4 ) );

notation
let c1 be AffinSpace;
let c2 be Subset of c1;
synonym c2 is_line for being_line c2;
end;

Lemma25: for b1 being AffinSpace
for b2, b3 being Element of b1
for b4 being Subset of b1 holds
( b4 is_line & b2 in b4 & b3 in b4 & b2 <> b3 implies b4 = Line b2,b3 )
proof
let c1 be AffinSpace;
let c2, c3 be Element of c1;
let c4 be Subset of c1;
assume that
E26: c4 is_line and
E27: ( c2 in c4 & c3 in c4 & c2 <> c3 ) ;
E28: ex b1, b2 being Element of c1 st
( b1 <> b2 & c4 = Line b1,b2 ) by E26, Def3;
then E29: Line c2,c3 c= c4 by E27, Th27;
c4 c= Line c2,c3 by E27, E28, Th28;
hence c4 = Line c2,c3 by E29, XBOOLE_0:def 10;
end;

theorem Th29: :: AFF_1:29
canceled;

theorem Th30: :: AFF_1:30
for b1 being AffinSpace
for b2, b3 being Element of b1
for b4, b5 being Subset of b1 holds
not ( b4 is_line & b5 is_line & b2 in b4 & b3 in b4 & b2 in b5 & b3 in b5 & not b2 = b3 & not b4 = b5 )
proof
let c1 be AffinSpace;
let c2, c3 be Element of c1;
let c4, c5 be Subset of c1;
assume E27: ( c4 is_line & c5 is_line & c2 in c4 & c3 in c4 & c2 in c5 & c3 in c5 ) ;
assume c2 <> c3 ;
then ( c4 = Line c2,c3 & c5 = Line c2,c3 ) by E27, Lemma25;
hence c4 = c5 ;
end;

theorem Th31: :: AFF_1:31
for b1 being AffinSpace
for b2 being Subset of b1 holds
not ( b2 is_line & ( for b3, b4 being Element of b1 holds
not ( b3 in b2 & b4 in b2 & b3 <> b4 ) ) )
proof
let c1 be AffinSpace;
let c2 be Subset of c1;
assume c2 is_line ;
then consider c3, c4 being Element of c1 such that
E28: ( c3 <> c4 & c2 = Line c3,c4 ) by Def3;
( c3 in c2 & c4 in c2 ) by E28, Th26;
hence ex b1, b2 being Element of c1 st
( b1 in c2 & b2 in c2 & b1 <> b2 ) by E28;
end;

theorem Th32: :: AFF_1:32
for b1 being AffinSpace
for b2 being Element of b1
for b3 being Subset of b1 holds
not ( b3 is_line & ( for b4 being Element of b1 holds
not ( b2 <> b4 & b4 in b3 ) ) )
proof
let c1 be AffinSpace;
let c2 be Element of c1;
let c3 be Subset of c1;
assume c3 is_line ;
then consider c4, c5 being Element of c1 such that
E29: ( c4 in c3 & c5 in c3 & c4 <> c5 ) by Th31;
( c2 = c4 implies ( c2 <> c5 & c5 in c3 ) ) by E29;
hence ex b1 being Element of c1 st
( c2 <> b1 & b1 in c3 ) by E29;
end;

theorem Th33: :: AFF_1:33
for b1 being AffinSpace
for b2, b3, b4 being Element of b1 holds
( LIN b2,b3,b4 iff ex b5 being Subset of b1 st
( b5 is_line & b2 in b5 & b3 in b5 & b4 in b5 ) )
proof
let c1 be AffinSpace;
let c2, c3, c4 be Element of c1;
E30: not ( LIN c2,c3,c4 & ( for b1 being Subset of c1 holds
not ( b1 is_line & c2 in b1 & c3 in b1 & c4 in b1 ) ) )
proof
assume E31: LIN c2,c3,c4 ;
E32: now
assume E33: ( c2 = c3 & c2 = c4 ) ;
consider c5 being Element of c1 such that
E34: c2 <> c5 by Th10;
set c6 = Line c2,c5;
( Line c2,c5 is_line & c2 in Line c2,c5 & c3 in Line c2,c5 & c4 in Line c2,c5 ) by E33, E34, Def3, Th26;
hence ex b1 being Subset of c1 st
( b1 is_line & c2 in b1 & c3 in b1 & c4 in b1 ) ;
end;
E33: now
assume E34: c2 <> c3 ;
set c5 = Line c2,c3;
( Line c2,c3 is_line & c2 in Line c2,c3 & c3 in Line c2,c3 & c4 in Line c2,c3 ) by E31, E34, Def2, Def3, Th26;
hence ex b1 being Subset of c1 st
( b1 is_line & c2 in b1 & c3 in b1 & c4 in b1 ) ;
end;
now
assume E34: c2 <> c4 ;
E35: LIN c2,c4,c3 by E31, Th15;
set c5 = Line c2,c4;
( Line c2,c4 is_line & c2 in Line c2,c4 & c3 in Line c2,c4 & c4 in Line c2,c4 ) by E34, E35, Def2, Def3, Th26;
hence ex b1 being Subset of c1 st
( b1 is_line & c2 in b1 & c3 in b1 & c4 in b1 ) ;
end;
hence ex b1 being Subset of c1 st
( b1 is_line & c2 in b1 & c3 in b1 & c4 in b1 ) by E32, E33;
end;
( ex b1 being Subset of c1 st
( b1 is_line & c2 in b1 & c3 in b1 & c4 in b1 ) implies LIN c2,c3,c4 )
proof
given c5 being Subset of c1 such that E31: c5 is_line and
E32: ( c2 in c5 & c3 in c5 & c4 in c5 ) ;
consider c6, c7 being Element of c1 such that
E33: ( c6 <> c7 & c5 = Line c6,c7 ) by E31, Def3;
( LIN c6,c7,c2 & LIN c6,c7,c3 & LIN c6,c7,c4 ) by E32, E33, Def2;
hence LIN c2,c3,c4 by E33, Th17;
end;
hence ( LIN c2,c3,c4 iff ex b1 being Subset of c1 st
( b1 is_line & c2 in b1 & c3 in b1 & c4 in b1 ) ) by E30;
end;

definition
let c1 be AffinSpace;
let c2, c3 be Element of c1;
let c4 be Subset of c1;
pred c2,c3 // c4 means :Def4: :: AFF_1:def 4
ex b1, b2 being Element of a1 st
( b1 <> b2 & a4 = Line b1,b2 & a2,a3 // b1,b2 );
end;

:: deftheorem Def4 defines // AFF_1:def 4 :
for b1 being AffinSpace
for b2, b3 being Element of b1
for b4 being Subset of b1 holds
( b2,b3 // b4 iff ex b5, b6 being Element of b1 st
( b5 <> b6 & b4 = Line b5,b6 & b2,b3 // b5,b6 ) );

definition
let c1 be AffinSpace;
let c2, c3 be Subset of c1;
pred c2 // c3 means :Def5: :: AFF_1:def 5
ex b1, b2 being Element of a1 st
( a2 = Line b1,b2 & b1 <> b2 & b1,b2 // a3 );
end;

:: deftheorem Def5 defines // AFF_1:def 5 :
for b1 being AffinSpace
for b2, b3 being Subset of b1 holds
( b2 // b3 iff ex b4, b5 being Element of b1 st
( b2 = Line b4,b5 & b4 <> b5 & b4,b5 // b3 ) );

theorem Th34: :: AFF_1:34
canceled;

theorem Th35: :: AFF_1:35
canceled;

theorem Th36: :: AFF_1:36
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1 holds
( b2 in Line b3,b4 & b3 <> b4 implies ( b5 in Line b3,b4 iff b3,b4 // b2,b5 ) )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5 be Element of c1;
assume E33: ( c2 in Line c3,c4 & c3 <> c4 ) ;
then E34: LIN c3,c4,c2 by Def2;
E35: ( c5 in Line c3,c4 implies c3,c4 // c2,c5 )
proof
assume c5 in Line c3,c4 ;
then LIN c3,c4,c5 by Def2;
hence c3,c4 // c2,c5 by E34, Th19;
end;
( c3,c4 // c2,c5 implies c5 in Line c3,c4 )
proof
assume c3,c4 // c2,c5 ;
then LIN c3,c4,c5 by E33, E34, Th18;
hence c5 in Line c3,c4 by Def2;
end;
hence ( c5 in Line c3,c4 iff c3,c4 // c2,c5 ) by E35;
end;

theorem Th37: :: AFF_1:37
for b1 being AffinSpace
for b2, b3 being Element of b1
for b4 being Subset of b1 holds
( b4 is_line & b2 in b4 implies ( b3 in b4 iff b2,b3 // b4 ) )
proof
let c1 be AffinSpace;
let c2, c3 be Element of c1;
let c4 be Subset of c1;
assume E34: ( c4 is_line & c2 in c4 ) ;
E35: now
assume E36: c3 in c4 ;
consider c5, c6 being Element of c1 such that
E37: ( c5 <> c6 & c4 = Line c5,c6 ) by E34, Def3;
c5,c6 // c2,c3 by E34, E36, E37, Th36;
then c2,c3 // c5,c6 by Th13;
hence c2,c3 // c4 by E37, Def4;
end;
now
assume c2,c3 // c4 ;
then consider c5, c6 being Element of c1 such that
E36: ( c5 <> c6 & c4 = Line c5,c6 & c2,c3 // c5,c6 ) by Def4;
c5,c6 // c2,c3 by E36, Th13;
hence c3 in c4 by E34, E36, Th36;
end;
hence ( c3 in c4 iff c2,c3 // c4 ) by E35;
end;

theorem Th38: :: AFF_1:38
for b1 being AffinSpace
for b2, b3 being Element of b1
for b4 being Subset of b1 holds
( ( b2 <> b3 & b4 = Line b2,b3 implies ( b4 is_line & b2 in b4 & b3 in b4 & b2 <> b3 ) ) & ( b4 is_line & b2 in b4 & b3 in b4 & b2 <> b3 implies ( b2 <> b3 & b4 = Line b2,b3 ) ) ) by Def3, Lemma25, Th26;

theorem Th39: :: AFF_1:39
for b1 being AffinSpace
for b2, b3, b4 being Element of b1
for b5 being Subset of b1 holds
( b5 is_line & b2 in b5 & b3 in b5 & b2 <> b3 & LIN b2,b3,b4 implies b4 in b5 )
proof
let c1 be AffinSpace;
let c2, c3, c4 be Element of c1;
let c5 be Subset of c1;
assume that
E35: ( c5 is_line & c2 in c5 & c3 in c5 & c2 <> c3 ) and
E36: LIN c2,c3,c4 ;
c5 = Line c2,c3 by E35, Lemma25;
hence c4 in c5 by E36, Def2;
end;

theorem Th40: :: AFF_1:40
for b1 being AffinSpace
for b2 being Subset of b1 holds
( ex b3, b4 being Element of b1 st b3,b4 // b2 implies b2 is_line )
proof
let c1 be AffinSpace;
let c2 be Subset of c1;
given c3, c4 being Element of c1 such that E36: c3,c4 // c2 ;
ex b1, b2 being Element of c1 st
( b1 <> b2 & c2 = Line b1,b2 & c3,c4 // b1,b2 ) by E36, Def4;
hence c2 is_line by Def3;
end;

theorem Th41: :: AFF_1:41
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1
for b6 being Subset of b1 holds
( b2 in b6 & b3 in b6 & b6 is_line & b2 <> b3 implies ( b4,b5 // b6 iff b4,b5 // b2,b3 ) )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5 be Element of c1;
let c6 be Subset of c1;
assume that
E37: ( c2 in c6 & c3 in c6 ) and
E38: c6 is_line and
E39: c2 <> c3 ;
E40: ( c4,c5 // c6 implies c4,c5 // c2,c3 )
proof
assume c4,c5 // c6 ;
then consider c7, c8 being Element of c1 such that
E41: ( c7 <> c8 & c6 = Line c7,c8 & c4,c5 // c7,c8 ) by Def4;
c7,c8 // c2,c3 by E37, E41, Th36;
hence c4,c5 // c2,c3 by E41, Th14;
end;
( c4,c5 // c2,c3 implies c4,c5 // c6 )
proof
assume E41: c4,c5 // c2,c3 ;
c6 = Line c2,c3 by E37, E38, E39, Lemma25;
hence c4,c5 // c6 by E39, E41, Def4;
end;
hence ( c4,c5 // c6 iff c4,c5 // c2,c3 ) by E40;
end;

theorem Th42: :: AFF_1:42
canceled;

theorem Th43: :: AFF_1:43
for b1 being AffinSpace
for b2, b3 being Element of b1 holds
( b2 <> b3 implies b2,b3 // Line b2,b3 )
proof
let c1 be AffinSpace;
let c2, c3 be Element of c1;
assume E38: c2 <> c3 ;
c2,c3 // c2,c3 by Th11;
hence c2,c3 // Line c2,c3 by E38, Def4;
end;

theorem Th44: :: AFF_1:44
for b1 being AffinSpace
for b2, b3 being Element of b1
for b4 being Subset of b1 holds
( b4 is_line implies ( b2,b3 // b4 iff ex b5, b6 being Element of b1 st
( b5 <> b6 & b5 in b4 & b6 in b4 & b2,b3 // b5,b6 ) ) )
proof
let c1 be AffinSpace;
let c2, c3 be Element of c1;
let c4 be Subset of c1;
assume E39: c4 is_line ;
E40: not ( c2,c3 // c4 & ( for b1, b2 being Element of c1 holds
not ( b1 <> b2 & b1 in c4 & b2 in c4 & c2,c3 // b1,b2 ) ) )
proof
assume c2,c3 // c4 ;
then consider c5, c6 being Element of c1 such that
E41: ( c5 <> c6 & c4 = Line c5,c6 & c2,c3 // c5,c6 ) by Def4;
( c5 <> c6 & c5 in c4 & c6 in c4 & c2,c3 // c5,c6 ) by E41, Th26;
hence ex b1, b2 being Element of c1 st
( b1 <> b2 & b1 in c4 & b2 in c4 & c2,c3 // b1,b2 ) ;
end;
( ex b1, b2 being Element of c1 st
( b1 <> b2 & b1 in c4 & b2 in c4 & c2,c3 // b1,b2 ) implies c2,c3 // c4 )
proof
assume ex b1, b2 being Element of c1 st
( b1 <> b2 & b1 in c4 & b2 in c4 & c2,c3 // b1,b2 ) ;
then consider c5, c6 being Element of c1 such that
E41: ( c5 <> c6 & c5 in c4 & c6 in c4 & c2,c3 // c5,c6 ) ;
c4 = Line c5,c6 by E39, E41, Lemma25;
hence c2,c3 // c4 by E41, Def4;
end;
hence ( c2,c3 // c4 iff ex b1, b2 being Element of c1 st
( b1 <> b2 & b1 in c4 & b2 in c4 & c2,c3 // b1,b2 ) ) by E40;
end;

theorem Th45: :: AFF_1:45
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1
for b6 being Subset of b1 holds
( b6 is_line & b2,b3 // b6 & b4,b5 // b6 implies b2,b3 // b4,b5 )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5 be Element of c1;
let c6 be Subset of c1;
assume that
E39: c6 is_line and
E40: ( c2,c3 // c6 & c4,c5 // c6 ) ;
consider c7, c8 being Element of c1 such that
E41: ( c7 <> c8 & c6 = Line c7,c8 & c2,c3 // c7,c8 ) by E40, Def4;
( c7 in c6 & c8 in c6 ) by E41, Th26;
then c4,c5 // c7,c8 by E39, E40, E41, Th41;
hence c2,c3 // c4,c5 by E41, Th14;
end;

theorem Th46: :: AFF_1:46
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1
for b6 being Subset of b1 holds
( b2,b3 // b6 & b2,b3 // b4,b5 & b2 <> b3 implies b4,b5 // b6 )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5 be Element of c1;
let c6 be Subset of c1;
assume E40: ( c2,c3 // c6 & c2,c3 // c4,c5 & c2 <> c3 ) ;
then E41: c6 is_line by Th40;
then consider c7, c8 being Element of c1 such that
E42: ( c7 <> c8 & c7 in c6 & c8 in c6 & c2,c3 // c7,c8 ) by E40, Th44;
( c7 <> c8 & c7 in c6 & c8 in c6 & c4,c5 // c7,c8 ) by E40, E42, Th14;
hence c4,c5 // c6 by E41, Th44;
end;

theorem Th47: :: AFF_1:47
for b1 being AffinSpace
for b2 being Element of b1
for b3 being Subset of b1 holds
( b3 is_line implies b2,b2 // b3 )
proof
let c1 be AffinSpace;
let c2 be Element of c1;
let c3 be Subset of c1;
assume c3 is_line ;
then consider c4, c5 being Element of c1 such that
<