:: AFF_1 semantic presentation

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

:: deftheorem E1 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 :: AFF_1:1
canceled;

theorem :: AFF_1:2
canceled;

theorem :: AFF_1:3
canceled;

theorem :: AFF_1:4
canceled;

theorem :: AFF_1:5
canceled;

theorem :: AFF_1:6
canceled;

theorem :: AFF_1:7
canceled;

theorem :: AFF_1:8
canceled;

theorem :: AFF_1:9
canceled;

theorem E2: :: 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 E3: :: 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;

E4: 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 E3;
hence c4,c5 // c2,c3 by E5, DIRAF:47;
end;
hence c4,c5 // c2,c3 by DIRAF:47;
end;

theorem E5: :: 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 E4;
end;

E6: 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 E3;
then ( c3,c2 // c4,c5 or c2 = c3 ) by DIRAF:47;
hence c3,c2 // c4,c5 by E5;
end;

E7: 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 E4;
then c5,c4 // c2,c3 by E6;
hence c2,c3 // c5,c4 by E4;
end;

theorem E8: :: 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 E6, E7;
hence c3,c2 // c5,c4 by E6;
thus c4,c5 // c2,c3 by E9, E4;
hence ( c4,c5 // c3,c2 & c5,c4 // c2,c3 ) by E6, E7;
hence c5,c4 // c3,c2 by E7;
end;

theorem E9: :: AFF_1:14
for b1 being AffinSpace
for b2, b3, b4, b5, b6, b7 being Element of b1 holds
( ( ) implies ( not b2 <> b3 or ( 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 ) ) or 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 E8;
hence c4,c5 // c6,c7 by DIRAF:47;
end;

E10: 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 E1;
then ( c2,c4 // c2,c3 & c3,c2 // c3,c4 ) by E8, DIRAF:47;
hence ( LIN c2,c4,c3 & LIN c3,c2,c4 ) by E1;
end;

theorem E11: :: 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 E10;
hence ( LIN c3,c4,c2 & LIN c4,c2,c3 ) by E10;
hence LIN c4,c3,c2 by E10;
end;

theorem E12: :: 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 E3, E5;
hence ( LIN c2,c2,c3 & LIN c2,c3,c3 & LIN c2,c3,c2 ) by E1;
end;

theorem E13: :: AFF_1:17
for b1 being AffinSpace
for b2, b3, b4, b5, b6 being Element of b1 holds
( ( LIN b2,b3,b4 & LIN b2,b3,b5 & LIN b2,b3,b6 ) implies ( not b2 <> b3 or 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, E1;
then c4,c5 // c4,c6 by E9;
hence LIN c4,c5,c6 by E1;
end;
now
assume E16: c2 <> c4 ;
( c2,c3 // c2,c4 & c2,c3 // c2,c5 & c2,c3 // c2,c6 ) by E14, E1;
then ( c2,c4 // c2,c5 & c2,c4 // c2,c6 ) by E14, E9;
then ( c4,c2 // c4,c5 & c4,c2 // c4,c6 ) by DIRAF:47;
then c4,c5 // c4,c6 by E16, E9;
hence LIN c4,c5,c6 by E1;
end;
hence LIN c4,c5,c6 by E15;
end;

theorem E14: :: AFF_1:18
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1 holds
( ( LIN b2,b3,b4 & b2,b3 // b4,b5 ) implies ( not b2 <> b3 or 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, E1;
then c2,c4 // c4,c5 by E15, E9;
then c4,c2 // c4,c5 by E8;
then LIN c4,c2,c5 by E1;
then ( LIN c2,c4,c5 & LIN c2,c4,c3 & LIN c2,c4,c2 ) by E15, E11, E12;
hence LIN c2,c3,c5 by E16, E13;
end;
hence LIN c2,c3,c5 by E15, E1;
end;

theorem E15: :: 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, E1;
then c2,c4 // c2,c5 by E17, E9;
then c4,c2 // c4,c5 by DIRAF:47;
then c2,c4 // c4,c5 by E8;
hence c2,c3 // c4,c5 by E18, E9;
end;
hence c2,c3 // c4,c5 ;
end;
hence c2,c3 // c4,c5 by E5;
end;

theorem E16: :: AFF_1:20
for b1 being AffinSpace
for b2, b3, b4, b5, b6 being Element of b1 holds
( ( LIN b4,b5,b2 & LIN b4,b5,b3 & LIN b2,b3,b6 ) implies ( not b2 <> b3 or 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 E12;
then ( LIN c3,c2,c5 & LIN c3,c2,c4 & LIN c3,c2,c6 ) by E17, E18, E11, E13;
hence LIN c4,c5,c6 by E17, E13;
end;
hence LIN c4,c5,c6 by E12;
end;

theorem E17: :: 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, E1;
hence not for b1, b2, b3 being Element of c1 holds LIN b1,b2,b3 ;
end;

theorem :: 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 E17;
( LIN c2,c3,c4 & LIN c2,c3,c5 & LIN c2,c3,c6 ) by E19;
hence not verum by E18, E20, E13;
end;

theorem :: AFF_1:23
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1 holds
( ( LIN b2,b4,b5 & b3,b4 // b3,b5 ) implies ( LIN b2,b3,b4 or 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, E1;
then ( LIN c4,c5,c3 & LIN c4,c5,c2 & LIN c4,c5,c4 ) by E18, E11, E12;
hence not verum by E18, E19, E13;
end;

definition
let c1 be AffinSpace;
let c2, c3 be Element of c1;
func Line a2,a3 -> Subset of a1 means :E18: :: 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 E18 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 ) );

E19: 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, E18;
then LIN c3,c2,c5 by E11;
hence c4 in Line c3,c2 by E18;
end;
hence Line c2,c3 c= Line c3,c2 by TARSKI:def 3;
end;

theorem :: AFF_1:24
canceled;

theorem E20: :: 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 E19;
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 a2,a3 -> Subset of a1;
commutativity
for b1, b2 being Element of c1 holds Line b1,b2 = Line b2,b1 by E20;
end;

theorem E21: :: 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 E12;
hence ( c2 in Line c2,c3 & c3 in Line c2,c3 ) by E18;
end;

theorem E22: :: 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 ) implies ( not b2 <> b5 or 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 E18;
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, E18;
then LIN c3,c4,c7 by E23, E24, E16;
hence c6 in Line c3,c4 by E18;
end;
hence Line c2,c5 c= Line c3,c4 by TARSKI:def 3;
end;

theorem E23: :: 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 ) implies ( not b3 <> b4 or 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 E18;
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, E18;
then LIN c2,c5,c7 by E24, E25, E13;
hence c6 in Line c2,c5 by E18;
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 :E24: :: AFF_1:def 3
ex b1, b2 being Element of a1 st
( b1 <> b2 & a2 = Line b1,b2 );
end;

:: deftheorem E24 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;
end;

E25: for b1 being AffinSpace
for b2, b3 being Element of b1
for b4 being Subset of b1 holds
( ( b4 is is_line & b2 in b4 & b3 in b4 ) implies ( not b2 <> b3 or 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 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, E24;
then E29: Line c2,c3 c= c4 by E27, E22;
c4 c= Line c2,c3 by E27, E28, E23;
hence c4 = Line c2,c3 by E29, XBOOLE_0:def 10;
end;

theorem :: AFF_1:29
canceled;

theorem E26: :: 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 is_line & b5 is 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 is_line & c5 is 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, E25;
hence c4 = c5 ;
end;

theorem E27: :: AFF_1:31
for b1 being AffinSpace
for b2 being Subset of b1 holds
not ( b2 is 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 is_line ;
then consider c3, c4 being Element of c1 such that
E28: ( c3 <> c4 & c2 = Line c3,c4 ) by E24;
( c3 in c2 & c4 in c2 ) by E28, E21;
hence ex b1, b2 being Element of c1 st
( b1 in c2 & b2 in c2 & b1 <> b2 ) by E28;
end;

theorem E28: :: AFF_1:32
for b1 being AffinSpace
for b2 being Element of b1
for b3 being Subset of b1 holds
not ( b3 is 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 is_line ;
then consider c4, c5 being Element of c1 such that
E29: ( c4 in c3 & c5 in c3 & c4 <> c5 ) by E27;
( 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 E29: :: 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 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 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 E2;
set c6 = Line c2,c5;
( Line c2,c5 is is_line & c2 in Line c2,c5 & c3 in Line c2,c5 & c4 in Line c2,c5 ) by E33, E34, E24, E21;
hence ex b1 being Subset of c1 st
( b1 is 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 is_line & c2 in Line c2,c3 & c3 in Line c2,c3 & c4 in Line c2,c3 ) by E31, E34, E18, E24, E21;
hence ex b1 being Subset of c1 st
( b1 is is_line & c2 in b1 & c3 in b1 & c4 in b1 ) ;
end;
now
assume E34: c2 <> c4 ;
E35: LIN c2,c4,c3 by E31, E11;
set c5 = Line c2,c4;
( Line c2,c4 is is_line & c2 in Line c2,c4 & c3 in Line c2,c4 & c4 in Line c2,c4 ) by E34, E35, E18, E24, E21;
hence ex b1 being Subset of c1 st
( b1 is is_line & c2 in b1 & c3 in b1 & c4 in b1 ) ;
end;
hence ex b1 being Subset of c1 st
( b1 is is_line & c2 in b1 & c3 in b1 & c4 in b1 ) by E32, E33;
end;
( ex b1 being Subset of c1 st
( b1 is 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 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, E24;
( LIN c6,c7,c2 & LIN c6,c7,c3 & LIN c6,c7,c4 ) by E32, E33, E18;
hence LIN c2,c3,c4 by E33, E13;
end;
hence ( LIN c2,c3,c4 iff ex b1 being Subset of c1 st
( b1 is 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 a2,a3 // a4 means :E30: :: AFF_1:def 4
ex b1, b2 being Element of a1 st
( b1 <> b2 & a4 = Line b1,b2 & a2,a3 // b1,b2 );
end;

:: deftheorem E30 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 a2 // a3 means :E31: :: AFF_1:def 5
ex b1, b2 being Element of a1 st
( a2 = Line b1,b2 & b1 <> b2 & b1,b2 // a3 );
end;

:: deftheorem E31 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 :: AFF_1:34
canceled;

theorem :: AFF_1:35
canceled;

theorem E32: :: AFF_1:36
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1 holds
( ( b2 in Line b3,b4 ) implies ( not b3 <> b4 or ( 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 E18;
E35: ( c5 in Line c3,c4 implies c3,c4 // c2,c5 )
proof
assume c5 in Line c3,c4 ;
then LIN c3,c4,c5 by E18;
hence c3,c4 // c2,c5 by E34, E15;
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, E14;
hence c5 in Line c3,c4 by E18;
end;
hence ( c5 in Line c3,c4 iff c3,c4 // c2,c5 ) by E35;
end;

theorem E33: :: AFF_1:37
for b1 being AffinSpace
for b2, b3 being Element of b1
for b4 being Subset of b1 holds
( ( b4 is 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 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, E24;
c5,c6 // c2,c3 by E34, E36, E37, E32;
then c2,c3 // c5,c6 by E8;
hence c2,c3 // c4 by E37, E30;
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 E30;
c5,c6 // c2,c3 by E36, E8;
hence c3 in c4 by E34, E36, E32;
end;
hence ( c3 in c4 iff c2,c3 // c4 ) by E35;
end;

theorem :: AFF_1:38
for b1 being AffinSpace
for b2, b3 being Element of b1
for b4 being Subset of b1 holds
( ( ( b4 = Line b2,b3 ) implies ( not b2 <> b3 or ( b4 is is_line & b2 in b4 & b3 in b4 & b2 <> b3 ) ) ) & ( ( b4 is is_line & b2 in b4 & b3 in b4 ) implies ( not b2 <> b3 or ( b2 <> b3 & b4 = Line b2,b3 ) ) ) ) by E24, E25, E21;

theorem E34: :: AFF_1:39
for b1 being AffinSpace
for b2, b3, b4 being Element of b1
for b5 being Subset of b1 holds
( ( b5 is is_line & b2 in b5 & b3 in b5 & LIN b2,b3,b4 ) implies ( not b2 <> b3 or 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 is_line & c2 in c5 & c3 in c5 & c2 <> c3 )
and E36: LIN c2,c3,c4 ;
c5 = Line c2,c3 by E35, E25;
hence c4 in c5 by E36, E18;
end;

theorem E35: :: 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 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, E30;
hence c2 is is_line by E24;
end;

theorem E36: :: 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 is_line ) implies ( not b2 <> b3 or ( 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 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 E30;
c7,c8 // c2,c3 by E37, E41, E32;
hence c4,c5 // c2,c3 by E41, E9;
end;
( c4,c5 // c2,c3 implies c4,c5 // c6 )
proof
assume E41: c4,c5 // c2,c3 ;
c6 = Line c2,c3 by E37, E38, E39, E25;
hence c4,c5 // c6 by E39, E41, E30;
end;
hence ( c4,c5 // c6 iff c4,c5 // c2,c3 ) by E40;
end;

theorem :: AFF_1:42
canceled;

theorem E37: :: 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 E3;
hence c2,c3 // Line c2,c3 by E38, E30;
end;

theorem E38: :: AFF_1:44
for b1 being AffinSpace
for b2, b3 being Element of b1
for b4 being Subset of b1 holds
( b4 is 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 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 E30;
( c5 <> c6 & c5 in c4 & c6 in c4 & c2,c3 // c5,c6 ) by E41, E21;
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, E25;
hence c2,c3 // c4 by E41, E30;
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 :: 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 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 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, E30;
( c7 in c6 & c8 in c6 ) by E41, E21;
then c4,c5 // c7,c8 by E39, E40, E41, E36;
hence c2,c3 // c4,c5 by E41, E9;
end;

theorem E39: :: 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 ) implies ( not b2 <> b3 or 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 is_line by E35;
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, E38;
( c7 <> c8 & c7 in c6 & c8 in c6 & c4,c5 // c7,c8 ) by E40, E42, E9;
hence c4,c5 // c6 by E41, E38;
end;

theorem E40: :: AFF_1:47
for b1 being AffinSpace
for b2 being Element of b1
for b3 being Subset of b1 holds
( b3 is 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 is_line ;
then consider c4, c5 being Element of c1 such that
E41: ( c4 <> c5 & c3 = Line c4,c5 ) by E24;
c2,c2 // c4,c5 by E5;
hence c2,c2 // c3 by E41, E30;
end;

theorem E41: :: AFF_1:48
for b1 being AffinSpace
for b2, b3 being Element of b1
for b4 being Subset of b1 holds
( b2,b3 // b4 implies b3,b2 // b4 )
proof
let c1 be AffinSpace;
let c2, c3 be Element of c1;
let c4 be Subset of c1;
assume E42: c2,c3 // c4 ;
now
assume E43: c2 <> c3 ;
c2,c3 // c3,c2 by E3;
hence c3,c2 // c4 by E42, E43, E39;
end;
hence c3,c2 // c4 by E42;
end;

theorem :: AFF_1:49
for b1 being AffinSpace
for b2, b3 being Element of b1
for b4 being Subset of b1 holds
not ( b2,b3 // b4 & not b2 in b4 & b3 in b4 )
proof
let c1 be AffinSpace;
let c2, c3 be Element of c1;
let c4 be Subset of c1;
assume E42: ( c2,c3 // c4 & not c2 in c4 & c3 in c4 ) ;
then E43: c4 is is_line by E35;
c3,c2 // c4 by E42, E41;
hence not verum by E42, E43, E33;
end;

theorem E42: :: AFF_1:50
for b1 being AffinSpace
for b2, b3 being Subset of b1 holds
( b2 // b3 implies ( b2 is is_line & b3 is is_line ) )
proof
let c1 be AffinSpace;
let c2, c3 be Subset of c1;
assume c2 // c3 ;
then ex b1, b2 being Element of c1 st
( c2 = Line b1,b2 & b1 <> b2 & b1,b2 // c3 ) by E31;
hence ( c2 is is_line & c3 is is_line ) by E24, E35;
end;

theorem E43: :: AFF_1:51
for b1 being AffinSpace
for b2, b3 being Subset of b1 holds
( b2 // b3 iff ex b4, b5, b6, b7 being Element of b1 st
( b4 <> b5 & b6 <> b7 & b4,b5 // b6,b7 & b2 = Line b4,b5 & b3 = Line b6,b7 ) )
proof
let c1 be AffinSpace;
let c2, c3 be Subset of c1;
E44: not ( c2 // c3 & for b1, b2, b3, b4 being Element of c1 holds
not ( b1 <> b2 & b3 <> b4 & b1,b2 // b3,b4 & c2 = Line b1,b2 & c3 = Line b3,b4 ) )
proof
assume c2 // c3 ;
then consider c4, c5 being Element of c1 such that
E45: ( c2 = Line c4,c5 & c4 <> c5 & c4,c5 // c3 ) by E31;
ex b1, b2 being Element of c1 st
( b1 <> b2 & c3 = Line b1,b2 & c4,c5 // b1,b2 ) by E45, E30;
hence ex b1, b2, b3, b4 being Element of c1 st
( b1 <> b2 & b3 <> b4 & b1,b2 // b3,b4 & c2 = Line b1,b2 & c3 = Line b3,b4 ) by E45;
end;
( ex b1, b2, b3, b4 being Element of c1 st
( b1 <> b2 & b3 <> b4 & b1,b2 // b3,b4 & c2 = Line b1,b2 & c3 = Line b3,b4 ) implies c2 // c3 )
proof
assume ex b1, b2, b3, b4 being Element of c1 st
( b1 <> b2 & b3 <> b4 & b1,b2 // b3,b4 & c2 = Line b1,b2 & c3 = Line b3,b4 ) ;
then consider c4, c5, c6, c7 being Element of c1 such that
E45: ( c4 <> c5 & c6 <> c7 & c4,c5 // c6,c7 & c2 = Line c4,c5 & c3 = Line c6,c7 ) ;
c4,c5 // c3 by E45, E30;
hence c2 // c3 by E45, E31;
end;
hence ( c2 // c3 iff ex b1, b2, b3, b4 being Element of c1 st
( b1 <> b2 & b3 <> b4 & b1,b2 // b3,b4 & c2 = Line b1,b2 & c3 = Line b3,b4 ) ) by E44;
end;

theorem E44: :: AFF_1:52
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1
for b6, b7 being Subset of b1 holds
( ( b6 is is_line & b7 is is_line & b2 in b6 & b3 in b6 & b4 in b7 & b5 in b7 ) implies ( not b2 <> b3 or not b4 <> b5 or ( b6 // b7 iff b2,b3 // b4,b5 ) ) )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5 be Element of c1;
let c6, c7 be Subset of c1;
assume E45: ( c6 is is_line & c7 is is_line & c2 in c6 & c3 in c6 & c4 in c7 & c5 in c7 & c2 <> c3 & c4 <> c5 ) ;
E46: ( c6 // c7 implies c2,c3 // c4,c5 )
proof
assume c6 // c7 ;
then consider c8, c9, c10, c11 being Element of c1 such that
E47: ( c8 <> c9 & c10 <> c11 & c8,c9 // c10,c11 & c6 = Line c8,c9 & c7 = Line c10,c11 ) by E43;
c8,c9 // c2,c3 by E45, E47, E32;
then ( c2,c3 // c10,c11 & c10,c11 // c4,c5 ) by E45, E47, E9, E32;
hence c2,c3 // c4,c5 by E47, E9;
end;
( c2,c3 // c4,c5 implies c6 // c7 )
proof
assume E47: c2,c3 // c4,c5 ;
( c6 = Line c2,c3 & c7 = Line c4,c5 ) by E45, E25;
hence c6 // c7 by E45, E47, E43;
end;
hence ( c6 // c7 iff c2,c3 // c4,c5 ) by E46;
end;

theorem E45: :: AFF_1:53
for b1 being AffinSpace
for b2, b3, b4, b5 being Element of b1
for b6, b7 being Subset of b1 holds
( ( b2 in b6 & b3 in b6 & b4 in b7 & b5 in b7 & b6 // b7 ) implies ( b2,b3 // b4,b5 ) )
proof
let c1 be AffinSpace;
let c2, c3, c4, c5 be Element of c1;
let c6, c7 be Subset of c1;
assume that E46: ( c2 in c6 & c3 in c6 & c4 in c7 & c5 in c7 )
and E47: c6 // c7 ;
now
assume E48: ( c2 <> c3 & c4 <> c5 ) ;
( c6 is is_line & c7 is is_line ) by E47, E42;
hence c2,c3 // c4,c5 by E46, E47, E48, E44;
end;
hence c2,c3 // c4,c5 by E5;
end;

theorem :: AFF_1:54
for b1 being AffinSpace
for b2, b3 being Element of b1
for b4, b5 being Subset of b1 holds
( ( b2 in b4 & b3<