:: AFF_1 semantic presentation begin definition let AS be AffinSpace; let a, b, c be Element of AS; pred LIN a,b,c means :Def1: :: AFF_1:def 1 a,b // a,c; end; :: deftheorem Def1 defines LIN AFF_1:def_1_:_ for AS being AffinSpace for a, b, c being Element of AS holds ( LIN a,b,c iff a,b // a,c ); theorem Th1: :: AFF_1:1 for AS being AffinSpace for a being Element of AS ex b being Element of AS st a <> b proof let AS be AffinSpace; ::_thesis: for a being Element of AS ex b being Element of AS st a <> b let a be Element of AS; ::_thesis: ex b being Element of AS st a <> b consider x, y being Element of AS such that A1: x <> y by DIRAF:40; ( a = x implies a <> y ) by A1; hence ex b being Element of AS st a <> b ; ::_thesis: verum end; theorem Th2: :: AFF_1:2 for AS being AffinSpace for x, y being Element of AS holds ( x,y // y,x & x,y // x,y ) proof let AS be AffinSpace; ::_thesis: for x, y being Element of AS holds ( x,y // y,x & x,y // x,y ) let x, y be Element of AS; ::_thesis: ( x,y // y,x & x,y // x,y ) thus x,y // y,x by DIRAF:40; ::_thesis: x,y // x,y thus x,y // x,y by DIRAF:40; ::_thesis: verum end; Lm1: for AS being AffinSpace for x, y, z, t being Element of AS st x,y // z,t holds z,t // x,y proof let AS be AffinSpace; ::_thesis: for x, y, z, t being Element of AS st x,y // z,t holds z,t // x,y let x, y, z, t be Element of AS; ::_thesis: ( x,y // z,t implies z,t // x,y ) assume A1: x,y // z,t ; ::_thesis: z,t // x,y now__::_thesis:_(_x_<>_y_implies_z,t_//_x,y_) assume A2: x <> y ; ::_thesis: z,t // x,y x,y // x,y by Th2; hence z,t // x,y by A1, A2, DIRAF:40; ::_thesis: verum end; hence z,t // x,y by DIRAF:40; ::_thesis: verum end; theorem Th3: :: AFF_1:3 for AS being AffinSpace for x, y, z being Element of AS holds ( x,y // z,z & z,z // x,y ) proof let AS be AffinSpace; ::_thesis: for x, y, z being Element of AS holds ( x,y // z,z & z,z // x,y ) let x, y, z be Element of AS; ::_thesis: ( x,y // z,z & z,z // x,y ) thus x,y // z,z by DIRAF:40; ::_thesis: z,z // x,y hence z,z // x,y by Lm1; ::_thesis: verum end; Lm2: for AS being AffinSpace for x, y, z, t being Element of AS st x,y // z,t holds y,x // z,t proof let AS be AffinSpace; ::_thesis: for x, y, z, t being Element of AS st x,y // z,t holds y,x // z,t let x, y, z, t be Element of AS; ::_thesis: ( x,y // z,t implies y,x // z,t ) assume A1: x,y // z,t ; ::_thesis: y,x // z,t x,y // y,x by Th2; then ( y,x // z,t or x = y ) by A1, DIRAF:40; hence y,x // z,t by Th3; ::_thesis: verum end; Lm3: for AS being AffinSpace for x, y, z, t being Element of AS st x,y // z,t holds x,y // t,z proof let AS be AffinSpace; ::_thesis: for x, y, z, t being Element of AS st x,y // z,t holds x,y // t,z let x, y, z, t be Element of AS; ::_thesis: ( x,y // z,t implies x,y // t,z ) assume x,y // z,t ; ::_thesis: x,y // t,z then z,t // x,y by Lm1; then t,z // x,y by Lm2; hence x,y // t,z by Lm1; ::_thesis: verum end; theorem Th4: :: AFF_1:4 for AS being AffinSpace for x, y, z, t being Element of AS st x,y // z,t holds ( x,y // t,z & y,x // z,t & y,x // t,z & z,t // x,y & z,t // y,x & t,z // x,y & t,z // y,x ) proof let AS be AffinSpace; ::_thesis: for x, y, z, t being Element of AS st x,y // z,t holds ( x,y // t,z & y,x // z,t & y,x // t,z & z,t // x,y & z,t // y,x & t,z // x,y & t,z // y,x ) let x, y, z, t be Element of AS; ::_thesis: ( x,y // z,t implies ( x,y // t,z & y,x // z,t & y,x // t,z & z,t // x,y & z,t // y,x & t,z // x,y & t,z // y,x ) ) assume A1: x,y // z,t ; ::_thesis: ( x,y // t,z & y,x // z,t & y,x // t,z & z,t // x,y & z,t // y,x & t,z // x,y & t,z // y,x ) hence ( x,y // t,z & y,x // z,t ) by Lm2, Lm3; ::_thesis: ( y,x // t,z & z,t // x,y & z,t // y,x & t,z // x,y & t,z // y,x ) hence y,x // t,z by Lm2; ::_thesis: ( z,t // x,y & z,t // y,x & t,z // x,y & t,z // y,x ) thus z,t // x,y by A1, Lm1; ::_thesis: ( z,t // y,x & t,z // x,y & t,z // y,x ) hence ( z,t // y,x & t,z // x,y ) by Lm2, Lm3; ::_thesis: t,z // y,x hence t,z // y,x by Lm3; ::_thesis: verum end; theorem Th5: :: AFF_1:5 for AS being AffinSpace for a, b, x, y, z, t being Element of AS st a <> b & ( ( a,b // x,y & a,b // z,t ) or ( a,b // x,y & z,t // a,b ) or ( x,y // a,b & z,t // a,b ) or ( x,y // a,b & a,b // z,t ) ) holds x,y // z,t proof let AS be AffinSpace; ::_thesis: for a, b, x, y, z, t being Element of AS st a <> b & ( ( a,b // x,y & a,b // z,t ) or ( a,b // x,y & z,t // a,b ) or ( x,y // a,b & z,t // a,b ) or ( x,y // a,b & a,b // z,t ) ) holds x,y // z,t let a, b, x, y, z, t be Element of AS; ::_thesis: ( a <> b & ( ( a,b // x,y & a,b // z,t ) or ( a,b // x,y & z,t // a,b ) or ( x,y // a,b & z,t // a,b ) or ( x,y // a,b & a,b // z,t ) ) implies x,y // z,t ) assume that A1: a <> b and A2: ( ( a,b // x,y & a,b // z,t ) or ( a,b // x,y & z,t // a,b ) or ( x,y // a,b & z,t // a,b ) or ( x,y // a,b & a,b // z,t ) ) ; ::_thesis: x,y // z,t A3: a,b // z,t by A2, Th4; a,b // x,y by A2, Th4; hence x,y // z,t by A1, A3, DIRAF:40; ::_thesis: verum end; Lm4: for AS being AffinSpace for x, y, z being Element of AS st LIN x,y,z holds ( LIN x,z,y & LIN y,x,z ) proof let AS be AffinSpace; ::_thesis: for x, y, z being Element of AS st LIN x,y,z holds ( LIN x,z,y & LIN y,x,z ) let x, y, z be Element of AS; ::_thesis: ( LIN x,y,z implies ( LIN x,z,y & LIN y,x,z ) ) assume LIN x,y,z ; ::_thesis: ( LIN x,z,y & LIN y,x,z ) then A1: x,y // x,z by Def1; then A2: y,x // y,z by DIRAF:40; x,z // x,y by A1, Th4; hence ( LIN x,z,y & LIN y,x,z ) by A2, Def1; ::_thesis: verum end; theorem Th6: :: AFF_1:6 for AS being AffinSpace for x, y, z being Element of AS st LIN x,y,z holds ( LIN x,z,y & LIN y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x ) proof let AS be AffinSpace; ::_thesis: for x, y, z being Element of AS st LIN x,y,z holds ( LIN x,z,y & LIN y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x ) let x, y, z be Element of AS; ::_thesis: ( LIN x,y,z implies ( LIN x,z,y & LIN y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x ) ) assume LIN x,y,z ; ::_thesis: ( LIN x,z,y & LIN y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x ) hence ( LIN x,z,y & LIN y,x,z ) by Lm4; ::_thesis: ( LIN y,z,x & LIN z,x,y & LIN z,y,x ) hence ( LIN y,z,x & LIN z,x,y ) by Lm4; ::_thesis: LIN z,y,x hence LIN z,y,x by Lm4; ::_thesis: verum end; theorem Th7: :: AFF_1:7 for AS being AffinSpace for x, y being Element of AS holds ( LIN x,x,y & LIN x,y,y & LIN x,y,x ) proof let AS be AffinSpace; ::_thesis: for x, y being Element of AS holds ( LIN x,x,y & LIN x,y,y & LIN x,y,x ) let x, y be Element of AS; ::_thesis: ( LIN x,x,y & LIN x,y,y & LIN x,y,x ) A1: x,y // x,y by Th2; A2: x,y // x,x by Th3; x,x // x,y by Th3; hence ( LIN x,x,y & LIN x,y,y & LIN x,y,x ) by A1, A2, Def1; ::_thesis: verum end; theorem Th8: :: AFF_1:8 for AS being AffinSpace for x, y, z, t, u being Element of AS st x <> y & LIN x,y,z & LIN x,y,t & LIN x,y,u holds LIN z,t,u proof let AS be AffinSpace; ::_thesis: for x, y, z, t, u being Element of AS st x <> y & LIN x,y,z & LIN x,y,t & LIN x,y,u holds LIN z,t,u let x, y, z, t, u be Element of AS; ::_thesis: ( x <> y & LIN x,y,z & LIN x,y,t & LIN x,y,u implies LIN z,t,u ) assume that A1: x <> y and A2: LIN x,y,z and A3: LIN x,y,t and A4: LIN x,y,u ; ::_thesis: LIN z,t,u A5: now__::_thesis:_(_x_<>_z_implies_LIN_z,t,u_) A6: x,y // x,z by A2, Def1; x,y // x,u by A4, Def1; then x,z // x,u by A1, A6, Th5; then A7: z,x // z,u by DIRAF:40; x,y // x,t by A3, Def1; then x,z // x,t by A1, A6, Th5; then A8: z,x // z,t by DIRAF:40; assume x <> z ; ::_thesis: LIN z,t,u then z,t // z,u by A8, A7, Th5; hence LIN z,t,u by Def1; ::_thesis: verum end; now__::_thesis:_(_x_=_z_implies_LIN_z,t,u_) assume A9: x = z ; ::_thesis: LIN z,t,u then A10: z,y // z,u by A4, Def1; z,y // z,t by A3, A9, Def1; then z,t // z,u by A1, A9, A10, Th5; hence LIN z,t,u by Def1; ::_thesis: verum end; hence LIN z,t,u by A5; ::_thesis: verum end; theorem Th9: :: AFF_1:9 for AS being AffinSpace for x, y, z, t being Element of AS st x <> y & LIN x,y,z & x,y // z,t holds LIN x,y,t proof let AS be AffinSpace; ::_thesis: for x, y, z, t being Element of AS st x <> y & LIN x,y,z & x,y // z,t holds LIN x,y,t let x, y, z, t be Element of AS; ::_thesis: ( x <> y & LIN x,y,z & x,y // z,t implies LIN x,y,t ) assume that A1: x <> y and A2: LIN x,y,z and A3: x,y // z,t ; ::_thesis: LIN x,y,t now__::_thesis:_(_z_<>_x_implies_LIN_x,y,t_) x,y // x,z by A2, Def1; then x,z // z,t by A1, A3, Th5; then z,x // z,t by Th4; then LIN z,x,t by Def1; then A4: LIN x,z,t by Th6; assume A5: z <> x ; ::_thesis: LIN x,y,t A6: LIN x,z,x by Th7; LIN x,z,y by A2, Th6; hence LIN x,y,t by A5, A4, A6, Th8; ::_thesis: verum end; hence LIN x,y,t by A3, Def1; ::_thesis: verum end; theorem Th10: :: AFF_1:10 for AS being AffinSpace for x, y, z, t being Element of AS st LIN x,y,z & LIN x,y,t holds x,y // z,t proof let AS be AffinSpace; ::_thesis: for x, y, z, t being Element of AS st LIN x,y,z & LIN x,y,t holds x,y // z,t let x, y, z, t be Element of AS; ::_thesis: ( LIN x,y,z & LIN x,y,t implies x,y // z,t ) assume that A1: LIN x,y,z and A2: LIN x,y,t ; ::_thesis: x,y // z,t now__::_thesis:_(_x_<>_y_implies_x,y_//_z,t_) A3: x,y // x,t by A2, Def1; A4: x,y // x,z by A1, Def1; assume x <> y ; ::_thesis: x,y // z,t then x,z // x,t by A4, A3, Th5; then z,x // z,t by DIRAF:40; then x,z // z,t by Th4; hence x,y // z,t by A4, A3, Th5; ::_thesis: verum end; hence x,y // z,t by Th3; ::_thesis: verum end; theorem Th11: :: AFF_1:11 for AS being AffinSpace for u, z, x, y, w being Element of AS st u <> z & LIN x,y,u & LIN x,y,z & LIN u,z,w holds LIN x,y,w proof let AS be AffinSpace; ::_thesis: for u, z, x, y, w being Element of AS st u <> z & LIN x,y,u & LIN x,y,z & LIN u,z,w holds LIN x,y,w let u, z, x, y, w be Element of AS; ::_thesis: ( u <> z & LIN x,y,u & LIN x,y,z & LIN u,z,w implies LIN x,y,w ) assume that A1: u <> z and A2: LIN x,y,u and A3: LIN x,y,z and A4: LIN u,z,w ; ::_thesis: LIN x,y,w now__::_thesis:_(_x_<>_y_implies_LIN_x,y,w_) assume A5: x <> y ; ::_thesis: LIN x,y,w LIN x,y,x by Th7; then A6: LIN z,u,x by A2, A3, A5, Th8; LIN x,y,y by Th7; then A7: LIN z,u,y by A2, A3, A5, Th8; LIN z,u,w by A4, Th6; hence LIN x,y,w by A1, A7, A6, Th8; ::_thesis: verum end; hence LIN x,y,w by Th7; ::_thesis: verum end; theorem Th12: :: AFF_1:12 for AS being AffinSpace holds not for x, y, z being Element of AS holds LIN x,y,z proof let AS be AffinSpace; ::_thesis: not for x, y, z being Element of AS holds LIN x,y,z consider x, y, z being Element of AS such that A1: not x,y // x,z by DIRAF:40; not LIN x,y,z by A1, Def1; hence not for x, y, z being Element of AS holds LIN x,y,z ; ::_thesis: verum end; theorem :: AFF_1:13 for AS being AffinSpace for x, y being Element of AS st x <> y holds ex z being Element of AS st not LIN x,y,z proof let AS be AffinSpace; ::_thesis: for x, y being Element of AS st x <> y holds ex z being Element of AS st not LIN x,y,z let x, y be Element of AS; ::_thesis: ( x <> y implies ex z being Element of AS st not LIN x,y,z ) assume A1: x <> y ; ::_thesis: not for z being Element of AS holds LIN x,y,z consider a, b, c being Element of AS such that A2: not LIN a,b,c by Th12; assume A3: for z being Element of AS holds LIN x,y,z ; ::_thesis: contradiction then A4: LIN x,y,b ; A5: LIN x,y,c by A3; LIN x,y,a by A3; hence contradiction by A1, A2, A4, A5, Th8; ::_thesis: verum end; theorem :: AFF_1:14 for AS being AffinSpace for o, a, b, b9 being Element of AS st not LIN o,a,b & LIN o,b,b9 & a,b // a,b9 holds b = b9 proof let AS be AffinSpace; ::_thesis: for o, a, b, b9 being Element of AS st not LIN o,a,b & LIN o,b,b9 & a,b // a,b9 holds b = b9 let o, a, b, b9 be Element of AS; ::_thesis: ( not LIN o,a,b & LIN o,b,b9 & a,b // a,b9 implies b = b9 ) assume that A1: not LIN o,a,b and A2: LIN o,b,b9 and A3: a,b // a,b9 ; ::_thesis: b = b9 LIN a,b,b9 by A3, Def1; then A4: LIN b,b9,a by Th6; A5: LIN b,b9,b by Th7; assume A6: b <> b9 ; ::_thesis: contradiction LIN b,b9,o by A2, Th6; hence contradiction by A1, A6, A4, A5, Th8; ::_thesis: verum end; definition let AS be AffinSpace; let a, b be Element of AS; func Line (a,b) -> Subset of AS means :Def2: :: AFF_1:def 2 for x being Element of AS holds ( x in it iff LIN a,b,x ); existence ex b1 being Subset of AS st for x being Element of AS holds ( x in b1 iff LIN a,b,x ) proof defpred S1[ set ] means for y being Element of AS st y = \$1 holds LIN a,b,y; consider X being Subset of AS such that A1: for x being set holds ( x in X iff ( x in the carrier of AS & S1[x] ) ) from SUBSET_1:sch_1(); take X ; ::_thesis: for x being Element of AS holds ( x in X iff LIN a,b,x ) let x be Element of AS; ::_thesis: ( x in X iff LIN a,b,x ) thus ( x in X implies LIN a,b,x ) by A1; ::_thesis: ( LIN a,b,x implies x in X ) assume LIN a,b,x ; ::_thesis: x in X then for y being Element of AS st y = x holds LIN a,b,y ; hence x in X by A1; ::_thesis: verum end; uniqueness for b1, b2 being Subset of AS st ( for x being Element of AS holds ( x in b1 iff LIN a,b,x ) ) & ( for x being Element of AS holds ( x in b2 iff LIN a,b,x ) ) holds b1 = b2 proof let X1, X2 be Subset of AS; ::_thesis: ( ( for x being Element of AS holds ( x in X1 iff LIN a,b,x ) ) & ( for x being Element of AS holds ( x in X2 iff LIN a,b,x ) ) implies X1 = X2 ) assume that A2: for x being Element of AS holds ( x in X1 iff LIN a,b,x ) and A3: for x being Element of AS holds ( x in X2 iff LIN a,b,x ) ; ::_thesis: X1 = X2 for x being set holds ( x in X1 iff x in X2 ) proof let x be set ; ::_thesis: ( x in X1 iff x in X2 ) thus ( x in X1 implies x in X2 ) ::_thesis: ( x in X2 implies x in X1 ) proof assume A4: x in X1 ; ::_thesis: x in X2 then reconsider x9 = x as Element of AS ; LIN a,b,x9 by A2, A4; hence x in X2 by A3; ::_thesis: verum end; assume A5: x in X2 ; ::_thesis: x in X1 then reconsider x9 = x as Element of AS ; LIN a,b,x9 by A3, A5; hence x in X1 by A2; ::_thesis: verum end; hence X1 = X2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def2 defines Line AFF_1:def_2_:_ for AS being AffinSpace for a, b being Element of AS for b4 being Subset of AS holds ( b4 = Line (a,b) iff for x being Element of AS holds ( x in b4 iff LIN a,b,x ) ); Lm5: for AS being AffinSpace for a, b being Element of AS holds Line (a,b) c= Line (b,a) proof let AS be AffinSpace; ::_thesis: for a, b being Element of AS holds Line (a,b) c= Line (b,a) let a, b be Element of AS; ::_thesis: Line (a,b) c= Line (b,a) now__::_thesis:_for_x_being_set_st_x_in_Line_(a,b)_holds_ x_in_Line_(b,a) let x be set ; ::_thesis: ( x in Line (a,b) implies x in Line (b,a) ) assume A1: x in Line (a,b) ; ::_thesis: x in Line (b,a) then reconsider x9 = x as Element of AS ; LIN a,b,x9 by A1, Def2; then LIN b,a,x9 by Th6; hence x in Line (b,a) by Def2; ::_thesis: verum end; hence Line (a,b) c= Line (b,a) by TARSKI:def_3; ::_thesis: verum end; definition let AS be AffinSpace; let a, b be Element of AS; :: original: Line redefine func Line (a,b) -> Subset of AS; commutativity for a, b being Element of AS holds Line (a,b) = Line (b,a) proof let a, b be Element of AS; ::_thesis: Line (a,b) = Line (b,a) A1: Line (b,a) c= Line (a,b) by Lm5; Line (a,b) c= Line (b,a) by Lm5; hence Line (a,b) = Line (b,a) by A1, XBOOLE_0:def_10; ::_thesis: verum end; end; theorem Th15: :: AFF_1:15 for AS being AffinSpace for a, b being Element of AS holds ( a in Line (a,b) & b in Line (a,b) ) proof let AS be AffinSpace; ::_thesis: for a, b being Element of AS holds ( a in Line (a,b) & b in Line (a,b) ) let a, b be Element of AS; ::_thesis: ( a in Line (a,b) & b in Line (a,b) ) A1: LIN a,b,b by Th7; LIN a,b,a by Th7; hence ( a in Line (a,b) & b in Line (a,b) ) by A1, Def2; ::_thesis: verum end; theorem Th16: :: AFF_1:16 for AS being AffinSpace for c, a, b, d being Element of AS st c in Line (a,b) & d in Line (a,b) & c <> d holds Line (c,d) c= Line (a,b) proof let AS be AffinSpace; ::_thesis: for c, a, b, d being Element of AS st c in Line (a,b) & d in Line (a,b) & c <> d holds Line (c,d) c= Line (a,b) let c, a, b, d be Element of AS; ::_thesis: ( c in Line (a,b) & d in Line (a,b) & c <> d implies Line (c,d) c= Line (a,b) ) assume that A1: c in Line (a,b) and A2: d in Line (a,b) and A3: c <> d ; ::_thesis: Line (c,d) c= Line (a,b) A4: LIN a,b,d by A2, Def2; A5: LIN a,b,c by A1, Def2; now__::_thesis:_for_x_being_set_st_x_in_Line_(c,d)_holds_ x_in_Line_(a,b) let x be set ; ::_thesis: ( x in Line (c,d) implies x in Line (a,b) ) assume A6: x in Line (c,d) ; ::_thesis: x in Line (a,b) then reconsider x9 = x as Element of AS ; LIN c,d,x9 by A6, Def2; then LIN a,b,x9 by A3, A5, A4, Th11; hence x in Line (a,b) by Def2; ::_thesis: verum end; hence Line (c,d) c= Line (a,b) by TARSKI:def_3; ::_thesis: verum end; theorem Th17: :: AFF_1:17 for AS being AffinSpace for c, a, b, d being Element of AS st c in Line (a,b) & d in Line (a,b) & a <> b holds Line (a,b) c= Line (c,d) proof let AS be AffinSpace; ::_thesis: for c, a, b, d being Element of AS st c in Line (a,b) & d in Line (a,b) & a <> b holds Line (a,b) c= Line (c,d) let c, a, b, d be Element of AS; ::_thesis: ( c in Line (a,b) & d in Line (a,b) & a <> b implies Line (a,b) c= Line (c,d) ) assume that A1: c in Line (a,b) and A2: d in Line (a,b) and A3: a <> b ; ::_thesis: Line (a,b) c= Line (c,d) A4: LIN a,b,d by A2, Def2; A5: LIN a,b,c by A1, Def2; now__::_thesis:_for_x_being_set_st_x_in_Line_(a,b)_holds_ x_in_Line_(c,d) let x be set ; ::_thesis: ( x in Line (a,b) implies x in Line (c,d) ) assume A6: x in Line (a,b) ; ::_thesis: x in Line (c,d) then reconsider x9 = x as Element of AS ; LIN a,b,x9 by A6, Def2; then LIN c,d,x9 by A3, A5, A4, Th8; hence x in Line (c,d) by Def2; ::_thesis: verum end; hence Line (a,b) c= Line (c,d) by TARSKI:def_3; ::_thesis: verum end; definition let AS be AffinSpace; let A be Subset of AS; attrA is being_line means :Def3: :: AFF_1:def 3 ex a, b being Element of AS st ( a <> b & A = Line (a,b) ); end; :: deftheorem Def3 defines being_line AFF_1:def_3_:_ for AS being AffinSpace for A being Subset of AS holds ( A is being_line iff ex a, b being Element of AS st ( a <> b & A = Line (a,b) ) ); registration let AS be AffinSpace; cluster being_line for M2(K24( the carrier of AS)); existence ex b1 being Subset of AS st b1 is being_line proof set a = the Element of AS; consider b being Element of AS such that A1: the Element of AS <> b by Th1; take Line ( the Element of AS,b) ; ::_thesis: Line ( the Element of AS,b) is being_line thus Line ( the Element of AS,b) is being_line by A1, Def3; ::_thesis: verum end; end; Lm6: for AS being AffinSpace for a, b being Element of AS for A being Subset of AS st A is being_line & a in A & b in A & a <> b holds A = Line (a,b) proof let AS be AffinSpace; ::_thesis: for a, b being Element of AS for A being Subset of AS st A is being_line & a in A & b in A & a <> b holds A = Line (a,b) let a, b be Element of AS; ::_thesis: for A being Subset of AS st A is being_line & a in A & b in A & a <> b holds A = Line (a,b) let A be Subset of AS; ::_thesis: ( A is being_line & a in A & b in A & a <> b implies A = Line (a,b) ) assume that A1: A is being_line and A2: a in A and A3: b in A and A4: a <> b ; ::_thesis: A = Line (a,b) A5: ex p, q being Element of AS st ( p <> q & A = Line (p,q) ) by A1, Def3; then A6: A c= Line (a,b) by A2, A3, Th17; Line (a,b) c= A by A2, A3, A4, A5, Th16; hence A = Line (a,b) by A6, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th18: :: AFF_1:18 for AS being AffinSpace for a, b being Element of AS for A, C being Subset of AS st A is being_line & C is being_line & a in A & b in A & a in C & b in C & not a = b holds A = C proof let AS be AffinSpace; ::_thesis: for a, b being Element of AS for A, C being Subset of AS st A is being_line & C is being_line & a in A & b in A & a in C & b in C & not a = b holds A = C let a, b be Element of AS; ::_thesis: for A, C being Subset of AS st A is being_line & C is being_line & a in A & b in A & a in C & b in C & not a = b holds A = C let A, C be Subset of AS; ::_thesis: ( A is being_line & C is being_line & a in A & b in A & a in C & b in C & not a = b implies A = C ) assume that A1: A is being_line and A2: C is being_line and A3: a in A and A4: b in A and A5: a in C and A6: b in C ; ::_thesis: ( a = b or A = C ) assume A7: a <> b ; ::_thesis: A = C then A = Line (a,b) by A1, A3, A4, Lm6; hence A = C by A2, A5, A6, A7, Lm6; ::_thesis: verum end; theorem Th19: :: AFF_1:19 for AS being AffinSpace for A being Subset of AS st A is being_line holds ex a, b being Element of AS st ( a in A & b in A & a <> b ) proof let AS be AffinSpace; ::_thesis: for A being Subset of AS st A is being_line holds ex a, b being Element of AS st ( a in A & b in A & a <> b ) let A be Subset of AS; ::_thesis: ( A is being_line implies ex a, b being Element of AS st ( a in A & b in A & a <> b ) ) assume A is being_line ; ::_thesis: ex a, b being Element of AS st ( a in A & b in A & a <> b ) then consider a, b being Element of AS such that A1: a <> b and A2: A = Line (a,b) by Def3; A3: b in A by A2, Th15; a in A by A2, Th15; hence ex a, b being Element of AS st ( a in A & b in A & a <> b ) by A1, A3; ::_thesis: verum end; theorem Th20: :: AFF_1:20 for AS being AffinSpace for a being Element of AS for A being Subset of AS st A is being_line holds ex b being Element of AS st ( a <> b & b in A ) proof let AS be AffinSpace; ::_thesis: for a being Element of AS for A being Subset of AS st A is being_line holds ex b being Element of AS st ( a <> b & b in A ) let a be Element of AS; ::_thesis: for A being Subset of AS st A is being_line holds ex b being Element of AS st ( a <> b & b in A ) let A be Subset of AS; ::_thesis: ( A is being_line implies ex b being Element of AS st ( a <> b & b in A ) ) assume A is being_line ; ::_thesis: ex b being Element of AS st ( a <> b & b in A ) then consider p, q being Element of AS such that A1: p in A and A2: q in A and A3: p <> q by Th19; ( a = p implies ( a <> q & q in A ) ) by A2, A3; hence ex b being Element of AS st ( a <> b & b in A ) by A1; ::_thesis: verum end; theorem Th21: :: AFF_1:21 for AS being AffinSpace for a, b, c being Element of AS holds ( LIN a,b,c iff ex A being Subset of AS st ( A is being_line & a in A & b in A & c in A ) ) proof let AS be AffinSpace; ::_thesis: for a, b, c being Element of AS holds ( LIN a,b,c iff ex A being Subset of AS st ( A is being_line & a in A & b in A & c in A ) ) let a, b, c be Element of AS; ::_thesis: ( LIN a,b,c iff ex A being Subset of AS st ( A is being_line & a in A & b in A & c in A ) ) A1: ( LIN a,b,c implies ex A being Subset of AS st ( A is being_line & a in A & b in A & c in A ) ) proof assume A2: LIN a,b,c ; ::_thesis: ex A being Subset of AS st ( A is being_line & a in A & b in A & c in A ) A3: now__::_thesis:_(_a_<>_b_implies_ex_A_being_Subset_of_AS_st_ (_A_is_being_line_&_a_in_A_&_b_in_A_&_c_in_A_)_) set A = Line (a,b); A4: a in Line (a,b) by Th15; A5: b in Line (a,b) by Th15; assume a <> b ; ::_thesis: ex A being Subset of AS st ( A is being_line & a in A & b in A & c in A ) then A6: Line (a,b) is being_line by Def3; c in Line (a,b) by A2, Def2; hence ex A being Subset of AS st ( A is being_line & a in A & b in A & c in A ) by A6, A4, A5; ::_thesis: verum end; A7: now__::_thesis:_(_a_<>_c_implies_ex_A_being_Subset_of_AS_st_ (_A_is_being_line_&_a_in_A_&_b_in_A_&_c_in_A_)_) set A = Line (a,c); A8: c in Line (a,c) by Th15; assume a <> c ; ::_thesis: ex A being Subset of AS st ( A is being_line & a in A & b in A & c in A ) then A9: Line (a,c) is being_line by Def3; LIN a,c,b by A2, Th6; then A10: b in Line (a,c) by Def2; a in Line (a,c) by Th15; hence ex A being Subset of AS st ( A is being_line & a in A & b in A & c in A ) by A9, A10, A8; ::_thesis: verum end; now__::_thesis:_(_a_=_b_&_a_=_c_implies_ex_A_being_Subset_of_AS_st_ (_A_is_being_line_&_a_in_A_&_b_in_A_&_c_in_A_)_) consider x being Element of AS such that A11: a <> x by Th1; set A = Line (a,x); A12: a in Line (a,x) by Th15; assume that A13: a = b and A14: a = c ; ::_thesis: ex A being Subset of AS st ( A is being_line & a in A & b in A & c in A ) Line (a,x) is being_line by A11, Def3; hence ex A being Subset of AS st ( A is being_line & a in A & b in A & c in A ) by A13, A14, A12; ::_thesis: verum end; hence ex A being Subset of AS st ( A is being_line & a in A & b in A & c in A ) by A3, A7; ::_thesis: verum end; ( ex A being Subset of AS st ( A is being_line & a in A & b in A & c in A ) implies LIN a,b,c ) proof given A being Subset of AS such that A15: A is being_line and A16: a in A and A17: b in A and A18: c in A ; ::_thesis: LIN a,b,c consider p, q being Element of AS such that A19: p <> q and A20: A = Line (p,q) by A15, Def3; A21: LIN p,q,b by A17, A20, Def2; A22: LIN p,q,c by A18, A20, Def2; LIN p,q,a by A16, A20, Def2; hence LIN a,b,c by A19, A21, A22, Th8; ::_thesis: verum end; hence ( LIN a,b,c iff ex A being Subset of AS st ( A is being_line & a in A & b in A & c in A ) ) by A1; ::_thesis: verum end; definition let AS be AffinSpace; let a, b be Element of AS; let A be Subset of AS; preda,b // A means :Def4: :: AFF_1:def 4 ex c, d being Element of AS st ( c <> d & A = Line (c,d) & a,b // c,d ); end; :: deftheorem Def4 defines // AFF_1:def_4_:_ for AS being AffinSpace for a, b being Element of AS for A being Subset of AS holds ( a,b // A iff ex c, d being Element of AS st ( c <> d & A = Line (c,d) & a,b // c,d ) ); definition let AS be AffinSpace; let A, C be Subset of AS; predA // C means :Def5: :: AFF_1:def 5 ex a, b being Element of AS st ( A = Line (a,b) & a <> b & a,b // C ); end; :: deftheorem Def5 defines // AFF_1:def_5_:_ for AS being AffinSpace for A, C being Subset of AS holds ( A // C iff ex a, b being Element of AS st ( A = Line (a,b) & a <> b & a,b // C ) ); theorem Th22: :: AFF_1:22 for AS being AffinSpace for c, a, b, d being Element of AS st c in Line (a,b) & a <> b holds ( d in Line (a,b) iff a,b // c,d ) proof let AS be AffinSpace; ::_thesis: for c, a, b, d being Element of AS st c in Line (a,b) & a <> b holds ( d in Line (a,b) iff a,b // c,d ) let c, a, b, d be Element of AS; ::_thesis: ( c in Line (a,b) & a <> b implies ( d in Line (a,b) iff a,b // c,d ) ) assume that A1: c in Line (a,b) and A2: a <> b ; ::_thesis: ( d in Line (a,b) iff a,b // c,d ) A3: LIN a,b,c by A1, Def2; thus ( d in Line (a,b) implies a,b // c,d ) ::_thesis: ( a,b // c,d implies d in Line (a,b) ) proof assume d in Line (a,b) ; ::_thesis: a,b // c,d then LIN a,b,d by Def2; hence a,b // c,d by A3, Th10; ::_thesis: verum end; assume a,b // c,d ; ::_thesis: d in Line (a,b) then LIN a,b,d by A2, A3, Th9; hence d in Line (a,b) by Def2; ::_thesis: verum end; theorem Th23: :: AFF_1:23 for AS being AffinSpace for a, b being Element of AS for A being Subset of AS st A is being_line & a in A holds ( b in A iff a,b // A ) proof let AS be AffinSpace; ::_thesis: for a, b being Element of AS for A being Subset of AS st A is being_line & a in A holds ( b in A iff a,b // A ) let a, b be Element of AS; ::_thesis: for A being Subset of AS st A is being_line & a in A holds ( b in A iff a,b // A ) let A be Subset of AS; ::_thesis: ( A is being_line & a in A implies ( b in A iff a,b // A ) ) assume that A1: A is being_line and A2: a in A ; ::_thesis: ( b in A iff a,b // A ) consider p, q being Element of AS such that A3: p <> q and A4: A = Line (p,q) by A1, Def3; hereby ::_thesis: ( a,b // A implies b in A ) assume b in A ; ::_thesis: a,b // A then p,q // a,b by A2, A3, A4, Th22; then a,b // p,q by Th4; hence a,b // A by A3, A4, Def4; ::_thesis: verum end; assume a,b // A ; ::_thesis: b in A then consider p, q being Element of AS such that A5: p <> q and A6: A = Line (p,q) and A7: a,b // p,q by Def4; p,q // a,b by A7, Th4; hence b in A by A2, A5, A6, Th22; ::_thesis: verum end; theorem :: AFF_1:24 for AS being AffinSpace for a, b being Element of AS for A being Subset of AS holds ( a <> b & A = Line (a,b) iff ( A is being_line & a in A & b in A & a <> b ) ) by Def3, Lm6, Th15; theorem Th25: :: AFF_1:25 for AS being AffinSpace for a, b, x being Element of AS for A being Subset of AS st A is being_line & a in A & b in A & a <> b & LIN a,b,x holds x in A proof let AS be AffinSpace; ::_thesis: for a, b, x being Element of AS for A being Subset of AS st A is being_line & a in A & b in A & a <> b & LIN a,b,x holds x in A let a, b, x be Element of AS; ::_thesis: for A being Subset of AS st A is being_line & a in A & b in A & a <> b & LIN a,b,x holds x in A let A be Subset of AS; ::_thesis: ( A is being_line & a in A & b in A & a <> b & LIN a,b,x implies x in A ) assume that A1: A is being_line and A2: a in A and A3: b in A and A4: a <> b and A5: LIN a,b,x ; ::_thesis: x in A A = Line (a,b) by A1, A2, A3, A4, Lm6; hence x in A by A5, Def2; ::_thesis: verum end; theorem Th26: :: AFF_1:26 for AS being AffinSpace for A being Subset of AS st ex a, b being Element of AS st a,b // A holds A is being_line proof let AS be AffinSpace; ::_thesis: for A being Subset of AS st ex a, b being Element of AS st a,b // A holds A is being_line let A be Subset of AS; ::_thesis: ( ex a, b being Element of AS st a,b // A implies A is being_line ) given a, b being Element of AS such that A1: a,b // A ; ::_thesis: A is being_line ex p, q being Element of AS st ( p <> q & A = Line (p,q) & a,b // p,q ) by A1, Def4; hence A is being_line by Def3; ::_thesis: verum end; theorem Th27: :: AFF_1:27 for AS being AffinSpace for c, d, a, b being Element of AS for A being Subset of AS st c in A & d in A & A is being_line & c <> d holds ( a,b // A iff a,b // c,d ) proof let AS be AffinSpace; ::_thesis: for c, d, a, b being Element of AS for A being Subset of AS st c in A & d in A & A is being_line & c <> d holds ( a,b // A iff a,b // c,d ) let c, d, a, b be Element of AS; ::_thesis: for A being Subset of AS st c in A & d in A & A is being_line & c <> d holds ( a,b // A iff a,b // c,d ) let A be Subset of AS; ::_thesis: ( c in A & d in A & A is being_line & c <> d implies ( a,b // A iff a,b // c,d ) ) assume that A1: c in A and A2: d in A and A3: A is being_line and A4: c <> d ; ::_thesis: ( a,b // A iff a,b // c,d ) thus ( a,b // A implies a,b // c,d ) ::_thesis: ( a,b // c,d implies a,b // A ) proof assume a,b // A ; ::_thesis: a,b // c,d then consider p, q being Element of AS such that A5: p <> q and A6: A = Line (p,q) and A7: a,b // p,q by Def4; p,q // c,d by A1, A2, A5, A6, Th22; hence a,b // c,d by A5, A7, Th5; ::_thesis: verum end; assume A8: a,b // c,d ; ::_thesis: a,b // A A = Line (c,d) by A1, A2, A3, A4, Lm6; hence a,b // A by A4, A8, Def4; ::_thesis: verum end; theorem Th28: :: AFF_1:28 for AS being AffinSpace for a, b being Element of AS for A being Subset of AS st a,b // A holds ex c, d being Element of AS st ( c <> d & c in A & d in A & a,b // c,d ) proof let AS be AffinSpace; ::_thesis: for a, b being Element of AS for A being Subset of AS st a,b // A holds ex c, d being Element of AS st ( c <> d & c in A & d in A & a,b // c,d ) let a, b be Element of AS; ::_thesis: for A being Subset of AS st a,b // A holds ex c, d being Element of AS st ( c <> d & c in A & d in A & a,b // c,d ) let A be Subset of AS; ::_thesis: ( a,b // A implies ex c, d being Element of AS st ( c <> d & c in A & d in A & a,b // c,d ) ) assume a,b // A ; ::_thesis: ex c, d being Element of AS st ( c <> d & c in A & d in A & a,b // c,d ) then consider c, d being Element of AS such that A1: c <> d and A2: A = Line (c,d) and A3: a,b // c,d by Def4; A4: d in A by A2, Th15; c in A by A2, Th15; hence ex c, d being Element of AS st ( c <> d & c in A & d in A & a,b // c,d ) by A1, A3, A4; ::_thesis: verum end; theorem Th29: :: AFF_1:29 for AS being AffinSpace for a, b being Element of AS st a <> b holds a,b // Line (a,b) proof let AS be AffinSpace; ::_thesis: for a, b being Element of AS st a <> b holds a,b // Line (a,b) let a, b be Element of AS; ::_thesis: ( a <> b implies a,b // Line (a,b) ) assume A1: a <> b ; ::_thesis: a,b // Line (a,b) a,b // a,b by Th2; hence a,b // Line (a,b) by A1, Def4; ::_thesis: verum end; theorem Th30: :: AFF_1:30 for AS being AffinSpace for a, b being Element of AS for A being being_line Subset of AS holds ( a,b // A iff ex c, d being Element of AS st ( c <> d & c in A & d in A & a,b // c,d ) ) proof let AS be AffinSpace; ::_thesis: for a, b being Element of AS for A being being_line Subset of AS holds ( a,b // A iff ex c, d being Element of AS st ( c <> d & c in A & d in A & a,b // c,d ) ) let a, b be Element of AS; ::_thesis: for A being being_line Subset of AS holds ( a,b // A iff ex c, d being Element of AS st ( c <> d & c in A & d in A & a,b // c,d ) ) A1: for A being Subset of AS st a,b // A holds ex c, d being Element of AS st ( c <> d & c in A & d in A & a,b // c,d ) by Th28; let A be being_line Subset of AS; ::_thesis: ( a,b // A iff ex c, d being Element of AS st ( c <> d & c in A & d in A & a,b // c,d ) ) ( ex c, d being Element of AS st ( c <> d & c in A & d in A & a,b // c,d ) implies a,b // A ) proof assume ex c, d being Element of AS st ( c <> d & c in A & d in A & a,b // c,d ) ; ::_thesis: a,b // A then consider c, d being Element of AS such that A2: c <> d and A3: c in A and A4: d in A and A5: a,b // c,d ; A = Line (c,d) by A2, A3, A4, Lm6; hence a,b // A by A2, A5, Def4; ::_thesis: verum end; hence ( a,b // A iff ex c, d being Element of AS st ( c <> d & c in A & d in A & a,b // c,d ) ) by A1; ::_thesis: verum end; theorem :: AFF_1:31 for AS being AffinSpace for a, b, c, d being Element of AS for A being being_line Subset of AS st a,b // A & c,d // A holds a,b // c,d proof let AS be AffinSpace; ::_thesis: for a, b, c, d being Element of AS for A being being_line Subset of AS st a,b // A & c,d // A holds a,b // c,d let a, b, c, d be Element of AS; ::_thesis: for A being being_line Subset of AS st a,b // A & c,d // A holds a,b // c,d let A be being_line Subset of AS; ::_thesis: ( a,b // A & c,d // A implies a,b // c,d ) assume that A1: a,b // A and A2: c,d // A ; ::_thesis: a,b // c,d consider p, q being Element of AS such that A3: p <> q and A4: A = Line (p,q) and A5: a,b // p,q by A1, Def4; A6: q in A by A4, Th15; p in A by A4, Th15; then c,d // p,q by A2, A3, A6, Th27; hence a,b // c,d by A3, A5, Th5; ::_thesis: verum end; theorem Th32: :: AFF_1:32 for AS being AffinSpace for a, b, p, q being Element of AS for A being Subset of AS st a,b // A & a,b // p,q & a <> b holds p,q // A proof let AS be AffinSpace; ::_thesis: for a, b, p, q being Element of AS for A being Subset of AS st a,b // A & a,b // p,q & a <> b holds p,q // A let a, b, p, q be Element of AS; ::_thesis: for A being Subset of AS st a,b // A & a,b // p,q & a <> b holds p,q // A let A be Subset of AS; ::_thesis: ( a,b // A & a,b // p,q & a <> b implies p,q // A ) assume that A1: a,b // A and A2: a,b // p,q and A3: a <> b ; ::_thesis: p,q // A A4: A is being_line by A1, Th26; then consider c, d being Element of AS such that A5: c <> d and A6: c in A and A7: d in A and A8: a,b // c,d by A1, Th30; p,q // c,d by A2, A3, A8, Th5; hence p,q // A by A4, A5, A6, A7, Th30; ::_thesis: verum end; theorem Th33: :: AFF_1:33 for AS being AffinSpace for a being Element of AS for A being being_line Subset of AS holds a,a // A proof let AS be AffinSpace; ::_thesis: for a being Element of AS for A being being_line Subset of AS holds a,a // A let a be Element of AS; ::_thesis: for A being being_line Subset of AS holds a,a // A let A be being_line Subset of AS; ::_thesis: a,a // A consider p, q being Element of AS such that A1: p <> q and A2: A = Line (p,q) by Def3; a,a // p,q by Th3; hence a,a // A by A1, A2, Def4; ::_thesis: verum end; theorem Th34: :: AFF_1:34 for AS being AffinSpace for a, b being Element of AS for A being Subset of AS st a,b // A holds b,a // A proof let AS be AffinSpace; ::_thesis: for a, b being Element of AS for A being Subset of AS st a,b // A holds b,a // A let a, b be Element of AS; ::_thesis: for A being Subset of AS st a,b // A holds b,a // A let A be Subset of AS; ::_thesis: ( a,b // A implies b,a // A ) assume A1: a,b // A ; ::_thesis: b,a // A now__::_thesis:_(_a_<>_b_implies_b,a_//_A_) assume A2: a <> b ; ::_thesis: b,a // A a,b // b,a by Th2; hence b,a // A by A1, A2, Th32; ::_thesis: verum end; hence b,a // A by A1; ::_thesis: verum end; theorem :: AFF_1:35 for AS being AffinSpace for a, b being Element of AS for A being Subset of AS st a,b // A & not a in A holds not b in A proof let AS be AffinSpace; ::_thesis: for a, b being Element of AS for A being Subset of AS st a,b // A & not a in A holds not b in A let a, b be Element of AS; ::_thesis: for A being Subset of AS st a,b // A & not a in A holds not b in A let A be Subset of AS; ::_thesis: ( a,b // A & not a in A implies not b in A ) assume that A1: a,b // A and A2: not a in A and A3: b in A ; ::_thesis: contradiction A4: b,a // A by A1, Th34; A is being_line by A1, Th26; hence contradiction by A2, A3, A4, Th23; ::_thesis: verum end; theorem Th36: :: AFF_1:36 for AS being AffinSpace for A, C being Subset of AS st A // C holds ( A is being_line & C is being_line ) proof let AS be AffinSpace; ::_thesis: for A, C being Subset of AS st A // C holds ( A is being_line & C is being_line ) let A, C be Subset of AS; ::_thesis: ( A // C implies ( A is being_line & C is being_line ) ) assume A // C ; ::_thesis: ( A is being_line & C is being_line ) then ex a, b being Element of AS st ( A = Line (a,b) & a <> b & a,b // C ) by Def5; hence ( A is being_line & C is being_line ) by Def3, Th26; ::_thesis: verum end; theorem Th37: :: AFF_1:37 for AS being AffinSpace for A, C being Subset of AS holds ( A // C iff ex a, b, c, d being Element of AS st ( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) ) ) proof let AS be AffinSpace; ::_thesis: for A, C being Subset of AS holds ( A // C iff ex a, b, c, d being Element of AS st ( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) ) ) let A, C be Subset of AS; ::_thesis: ( A // C iff ex a, b, c, d being Element of AS st ( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) ) ) thus ( A // C implies ex a, b, c, d being Element of AS st ( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) ) ) ::_thesis: ( ex a, b, c, d being Element of AS st ( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) ) implies A // C ) proof assume A // C ; ::_thesis: ex a, b, c, d being Element of AS st ( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) ) then consider a, b being Element of AS such that A1: A = Line (a,b) and A2: a <> b and A3: a,b // C by Def5; ex c, d being Element of AS st ( c <> d & C = Line (c,d) & a,b // c,d ) by A3, Def4; hence ex a, b, c, d being Element of AS st ( a <> b & c <> d & a,b // c,d & A = Line (a,b) & C = Line (c,d) ) by A1, A2; ::_thesis: verum end; given a, b, c, d being Element of AS such that A4: a <> b and A5: c <> d and A6: a,b // c,d and A7: A = Line (a,b) and A8: C = Line (c,d) ; ::_thesis: A // C a,b // C by A5, A6, A8, Def4; hence A // C by A4, A7, Def5; ::_thesis: verum end; theorem Th38: :: AFF_1:38 for AS being AffinSpace for a, b, c, d being Element of AS for A, C being being_line Subset of AS st a in A & b in A & c in C & d in C & a <> b & c <> d holds ( A // C iff a,b // c,d ) proof let AS be AffinSpace; ::_thesis: for a, b, c, d being Element of AS for A, C being being_line Subset of AS st a in A & b in A & c in C & d in C & a <> b & c <> d holds ( A // C iff a,b // c,d ) let a, b, c, d be Element of AS; ::_thesis: for A, C being being_line Subset of AS st a in A & b in A & c in C & d in C & a <> b & c <> d holds ( A // C iff a,b // c,d ) let A, C be being_line Subset of AS; ::_thesis: ( a in A & b in A & c in C & d in C & a <> b & c <> d implies ( A // C iff a,b // c,d ) ) assume that A1: a in A and A2: b in A and A3: c in C and A4: d in C and A5: a <> b and A6: c <> d ; ::_thesis: ( A // C iff a,b // c,d ) thus ( A // C implies a,b // c,d ) ::_thesis: ( a,b // c,d implies A // C ) proof assume A // C ; ::_thesis: a,b // c,d then consider p, q, r, s being Element of AS such that A7: p <> q and A8: r <> s and A9: p,q // r,s and A10: A = Line (p,q) and A11: C = Line (r,s) by Th37; p,q // a,b by A1, A2, A7, A10, Th22; then A12: a,b // r,s by A7, A9, Th5; r,s // c,d by A3, A4, A8, A11, Th22; hence a,b // c,d by A8, A12, Th5; ::_thesis: verum end; A13: C = Line (c,d) by A3, A4, A6, Lm6; assume A14: a,b // c,d ; ::_thesis: A // C A = Line (a,b) by A1, A2, A5, Lm6; hence A // C by A5, A6, A14, A13, Th37; ::_thesis: verum end; theorem Th39: :: AFF_1:39 for AS being AffinSpace for a, b, c, d being Element of AS for A, C being Subset of AS st a in A & b in A & c in C & d in C & A // C holds a,b // c,d proof let AS be AffinSpace; ::_thesis: for a, b, c, d being Element of AS for A, C being Subset of AS st a in A & b in A & c in C & d in C & A // C holds a,b // c,d let a, b, c, d be Element of AS; ::_thesis: for A, C being Subset of AS st a in A & b in A & c in C & d in C & A // C holds a,b // c,d let A, C be Subset of AS; ::_thesis: ( a in A & b in A & c in C & d in C & A // C implies a,b // c,d ) assume that A1: a in A and A2: b in A and A3: c in C and A4: d in C and A5: A // C ; ::_thesis: a,b // c,d now__::_thesis:_(_a_<>_b_&_c_<>_d_implies_a,b_//_c,d_) A6: C is being_line by A5, Th36; assume that A7: a <> b and A8: c <> d ; ::_thesis: a,b // c,d A is being_line by A5, Th36; hence a,b // c,d by A1, A2, A3, A4, A5, A7, A8, A6, Th38; ::_thesis: verum end; hence a,b // c,d by Th3; ::_thesis: verum end; theorem :: AFF_1:40 for AS being AffinSpace for a, b being Element of AS for A, C being Subset of AS st a in A & b in A & A // C holds a,b // C proof let AS be AffinSpace; ::_thesis: for a, b being Element of AS for A, C being Subset of AS st a in A & b in A & A // C holds a,b // C let a, b be Element of AS; ::_thesis: for A, C being Subset of AS st a in A & b in A & A // C holds a,b // C let A, C be Subset of AS; ::_thesis: ( a in A & b in A & A // C implies a,b // C ) assume that A1: a in A and A2: b in A and A3: A // C ; ::_thesis: a,b // C A4: C is being_line by A3, Th36; now__::_thesis:_a,b_//_C consider p, q being Element of AS such that A5: p in C and A6: q in C and A7: p <> q by A4, Th19; A8: C = Line (p,q) by A4, A5, A6, A7, Lm6; a,b // p,q by A1, A2, A3, A5, A6, Th39; hence a,b // C by A7, A8, Def4; ::_thesis: verum end; hence a,b // C ; ::_thesis: verum end; theorem Th41: :: AFF_1:41 for AS being AffinSpace for A being being_line Subset of AS holds A // A proof let AS be AffinSpace; ::_thesis: for A being being_line Subset of AS holds A // A let A be being_line Subset of AS; ::_thesis: A // A consider a, b being Element of AS such that A1: a <> b and A2: A = Line (a,b) by Def3; a,b // a,b by Th2; hence A // A by A1, A2, Th37; ::_thesis: verum end; definition let AS be AffinSpace; let A, B be being_line Subset of AS; :: original: // redefine predA // B; reflexivity for A being being_line Subset of AS holds (AS,b1,b1) by Th41; end; theorem Th42: :: AFF_1:42 for AS being AffinSpace for A, C being Subset of AS st A // C holds C // A proof let AS be AffinSpace; ::_thesis: for A, C being Subset of AS st A // C holds C // A let A, C be Subset of AS; ::_thesis: ( A // C implies C // A ) assume A // C ; ::_thesis: C // A then consider a, b, c, d being Element of AS such that A1: a <> b and A2: c <> d and A3: a,b // c,d and A4: A = Line (a,b) and A5: C = Line (c,d) by Th37; c,d // a,b by A3, Th4; hence C // A by A1, A2, A4, A5, Th37; ::_thesis: verum end; definition let AS be AffinSpace; let A, C be Subset of AS; :: original: // redefine predA // C; symmetry for A, C being Subset of AS st (AS,b1,b2) holds (AS,b2,b1) by Th42; end; theorem Th43: :: AFF_1:43 for AS being AffinSpace for a, b being Element of AS for A, C being Subset of AS st a,b // A & A // C holds a,b // C proof let AS be AffinSpace; ::_thesis: for a, b being Element of AS for A, C being Subset of AS st a,b // A & A // C holds a,b // C let a, b be Element of AS; ::_thesis: for A, C being Subset of AS st a,b // A & A // C holds a,b // C let A, C be Subset of AS; ::_thesis: ( a,b // A & A // C implies a,b // C ) assume that A1: a,b // A and A2: A // C ; ::_thesis: a,b // C consider p, q, c, d being Element of AS such that A3: p <> q and A4: c <> d and A5: p,q // c,d and A6: A = Line (p,q) and A7: C = Line (c,d) by A2, Th37; A8: q in A by A6, Th15; A9: A is being_line by A2, Th36; p in A by A6, Th15; then a,b // p,q by A1, A3, A8, A9, Th27; then a,b // c,d by A3, A5, Th5; hence a,b // C by A4, A7, Def4; ::_thesis: verum end; Lm7: for AS being AffinSpace for A, C, D being Subset of AS st A // C & C // D holds A // D proof let AS be AffinSpace; ::_thesis: for A, C, D being Subset of AS st A // C & C // D holds A // D let A, C, D be Subset of AS; ::_thesis: ( A // C & C // D implies A // D ) assume that A1: A // C and A2: C // D ; ::_thesis: A // D consider a, b, c, d being Element of AS such that A3: a <> b and A4: c <> d and A5: a,b // c,d and A6: A = Line (a,b) and A7: C = Line (c,d) by A1, Th37; A8: C is being_line by A2, Th36; A9: d in C by A7, Th15; A10: D is being_line by A2, Th36; then consider p, q being Element of AS such that A11: p <> q and A12: D = Line (p,q) by Def3; A13: p in D by A12, Th15; A14: q in D by A12, Th15; c in C by A7, Th15; then c,d // p,q by A2, A4, A8, A10, A11, A13, A14, A9, Th38; then a,b // p,q by A4, A5, Th5; hence A // D by A3, A6, A11, A12, Th37; ::_thesis: verum end; theorem :: AFF_1:44 for AS being AffinSpace for A, C, D being Subset of AS st ( ( A // C & C // D ) or ( A // C & D // C ) or ( C // A & C // D ) or ( C // A & D // C ) ) holds A // D by Lm7; theorem Th45: :: AFF_1:45 for AS being AffinSpace for p being Element of AS for A, C being Subset of AS st A // C & p in A & p in C holds A = C proof let AS be AffinSpace; ::_thesis: for p being Element of AS for A, C being Subset of AS st A // C & p in A & p in C holds A = C let p be Element of AS; ::_thesis: for A, C being Subset of AS st A // C & p in A & p in C holds A = C let A, C be Subset of AS; ::_thesis: ( A // C & p in A & p in C implies A = C ) assume that A1: A // C and A2: p in A and A3: p in C ; ::_thesis: A = C A4: for A, C being Subset of AS for p being Element of AS st A // C & p in A & p in C holds A c= C proof let A, C be Subset of AS; ::_thesis: for p being Element of AS st A // C & p in A & p in C holds A c= C let p be Element of AS; ::_thesis: ( A // C & p in A & p in C implies A c= C ) assume that A5: A // C and A6: p in A and A7: p in C ; ::_thesis: A c= C A8: C is being_line by A5, Th36; A9: A is being_line by A5, Th36; now__::_thesis:_for_x_being_set_st_x_in_A_holds_ x_in_C let x be set ; ::_thesis: ( x in A implies x in C ) assume A10: x in A ; ::_thesis: x in C then reconsider x9 = x as Element of AS ; now__::_thesis:_(_x9_<>_p_implies_x_in_C_) consider q being Element of AS such that A11: p <> q and A12: q in C by A8, Th20; assume A13: x9 <> p ; ::_thesis: x in C then A = Line (p,x9) by A6, A9, A10, Lm6; then p,x9 // C by A5, A13, Th29, Th43; then p,x9 // p,q by A7, A8, A11, A12, Th27; then p,q // p,x9 by Th4; then A14: LIN p,q,x9 by Def1; C = Line (p,q) by A7, A8, A11, A12, Lm6; hence x in C by A14, Def2; ::_thesis: verum end; hence x in C by A7; ::_thesis: verum end; hence A c= C by TARSKI:def_3; ::_thesis: verum end; then A15: C c= A by A1, A2, A3; A c= C by A1, A2, A3, A4; hence A = C by A15, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: AFF_1:46 for AS being AffinSpace for x, a, b being Element of AS for K being Subset of AS st x in K & not a in K & a,b // K & not a = b holds not LIN x,a,b proof let AS be AffinSpace; ::_thesis: for x, a, b being Element of AS for K being Subset of AS st x in K & not a in K & a,b // K & not a = b holds not LIN x,a,b let x, a, b be Element of AS; ::_thesis: for K being Subset of AS st x in K & not a in K & a,b // K & not a = b holds not LIN x,a,b let K be Subset of AS; ::_thesis: ( x in K & not a in K & a,b // K & not a = b implies not LIN x,a,b ) assume that A1: x in K and A2: not a in K and A3: a,b // K ; ::_thesis: ( a = b or not LIN x,a,b ) set A = Line (a,b); assume that A4: a <> b and A5: LIN x,a,b ; ::_thesis: contradiction LIN a,b,x by A5, Th6; then A6: x in Line (a,b) by Def2; A7: a in Line (a,b) by Th15; Line (a,b) // K by A3, A4, Def5; hence contradiction by A1, A2, A6, A7, Th45; ::_thesis: verum end; theorem :: AFF_1:47 for AS being AffinSpace for a9, b9, p, a, b being Element of AS for K being Subset of AS st a9,b9 // K & LIN p,a,a9 & LIN p,b,b9 & p in K & not a in K & a = b holds a9 = b9 proof let AS be AffinSpace; ::_thesis: for a9, b9, p, a, b being Element of AS for K being Subset of AS st a9,b9 // K & LIN p,a,a9 & LIN p,b,b9 & p in K & not a in K & a = b holds a9 = b9 let a9, b9, p, a, b be Element of AS; ::_thesis: for K being Subset of AS st a9,b9 // K & LIN p,a,a9 & LIN p,b,b9 & p in K & not a in K & a = b holds a9 = b9 let K be Subset of AS; ::_thesis: ( a9,b9 // K & LIN p,a,a9 & LIN p,b,b9 & p in K & not a in K & a = b implies a9 = b9 ) assume that A1: a9,b9 // K and A2: LIN p,a,a9 and A3: LIN p,b,b9 and A4: p in K and A5: not a in K and A6: a = b ; ::_thesis: a9 = b9 set A = Line (p,a); A7: b9 in Line (p,a) by A3, A6, Def2; A8: p in Line (p,a) by Th15; A9: a9 in Line (p,a) by A2, Def2; assume A10: a9 <> b9 ; ::_thesis: contradiction Line (p,a) is being_line by A4, A5, Def3; then Line (p,a) = Line (a9,b9) by A9, A7, A10, Lm6; then Line (p,a) // K by A1, A10, Def5; then Line (p,a) = K by A4, A8, Th45; hence contradiction by A5, Th15; ::_thesis: verum end; theorem :: AFF_1:48 for AS being AffinSpace for a, b, c, d being Element of AS for A being being_line Subset of AS st a in A & b in A & c in A & a <> b & a,b // c,d holds d in A proof let AS be AffinSpace; ::_thesis: for a, b, c, d being Element of AS for A being being_line Subset of AS st a in A & b in A & c in A & a <> b & a,b // c,d holds d in A let a, b, c, d be Element of AS; ::_thesis: for A being being_line Subset of AS st a in A & b in A & c in A & a <> b & a,b // c,d holds d in A let A be being_line Subset of AS; ::_thesis: ( a in A & b in A & c in A & a <> b & a,b // c,d implies d in A ) assume that A1: a in A and A2: b in A and A3: c in A and A4: a <> b and A5: a,b // c,d ; ::_thesis: d in A now__::_thesis:_(_c_<>_d_implies_d_in_A_) set C = Line (c,d); A6: c in Line (c,d) by Th15; A7: d in Line (c,d) by Th15; assume A8: c <> d ; ::_thesis: d in A then Line (c,d) is being_line by Def3; then A // Line (c,d) by A1, A2, A4, A5, A8, A6, A7, Th38; hence d in A by A3, A6, A7, Th45; ::_thesis: verum end; hence d in A by A3; ::_thesis: verum end; theorem :: AFF_1:49 for AS being AffinSpace for a being Element of AS for A being being_line Subset of AS ex C being Subset of AS st ( a in C & A // C ) proof let AS be AffinSpace; ::_thesis: for a being Element of AS for A being being_line Subset of AS ex C being Subset of AS st ( a in C & A // C ) let a be Element of AS; ::_thesis: for A being being_line Subset of AS ex C being Subset of AS st ( a in C & A // C ) let A be being_line Subset of AS; ::_thesis: ex C being Subset of AS st ( a in C & A // C ) consider p, q being Element of AS such that A1: p <> q and A2: A = Line (p,q) by Def3; consider b being Element of AS such that A3: p,q // a,b and A4: a <> b by DIRAF:40; set C = Line (a,b); A5: a in Line (a,b) by Th15; A // Line (a,b) by A1, A2, A3, A4, Th37; hence ex C being Subset of AS st ( a in C & A // C ) by A5; ::_thesis: verum end; theorem :: AFF_1:50 for AS being AffinSpace for p being Element of AS for A, C, D being Subset of AS st A // C & A // D & p in C & p in D holds C = D by Lm7, Th45; theorem :: AFF_1:51 for AS being AffinSpace for a, b, c, d being Element of AS for A being Subset of AS st A is being_line & a in A & b in A & c in A & d in A holds a,b // c,d by Th39, Th41; theorem :: AFF_1:52 for AS being AffinSpace for a, b being Element of AS for A being Subset of AS st A is being_line & a in A & b in A holds a,b // A by Th23; theorem :: AFF_1:53 for AS being AffinSpace for a, b being Element of AS for A, C being Subset of AS st a,b // A & a,b // C & a <> b holds A // C proof let AS be AffinSpace; ::_thesis: for a, b being Element of AS for A, C being Subset of AS st a,b // A & a,b // C & a <> b holds A // C let a, b be Element of AS; ::_thesis: for A, C being Subset of AS st a,b // A & a,b // C & a <> b holds A // C let A, C be Subset of AS; ::_thesis: ( a,b // A & a,b // C & a <> b implies A // C ) assume that A1: a,b // A and A2: a,b // C and A3: a <> b ; ::_thesis: A // C A4: C is being_line by A2, Th26; then consider p, q being Element of AS such that A5: p <> q and A6: p in C and A7: q in C and A8: a,b // p,q by A2, Th30; A9: A is being_line by A1, Th26; then consider c, d being Element of AS such that A10: c <> d and A11: c in A and A12: d in A and A13: a,b // c,d by A1, Th30; c,d // p,q by A3, A13, A8, Th5; hence A // C by A9, A4, A10, A11, A12, A5, A6, A7, Th38; ::_thesis: verum end; theorem Th54: :: AFF_1:54 for AS being AffinSpace for o, a, b, a9, b9 being Element of AS st not LIN o,a,b & LIN o,a,a9 & LIN o,b,b9 & a9 = b9 holds ( a9 = o & b9 = o ) proof let AS be AffinSpace; ::_thesis: for o, a, b, a9, b9 being Element of AS st not LIN o,a,b & LIN o,a,a9 & LIN o,b,b9 & a9 = b9 holds ( a9 = o & b9 = o ) let o, a, b, a9, b9 be Element of AS; ::_thesis: ( not LIN o,a,b & LIN o,a,a9 & LIN o,b,b9 & a9 = b9 implies ( a9 = o & b9 = o ) ) assume that A1: not LIN o,a,b and A2: LIN o,a,a9 and A3: LIN o,b,b9 and A4: a9 = b9 ; ::_thesis: ( a9 = o & b9 = o ) set A = Line (o,a); set C = Line (o,b); A5: o in Line (o,a) by Th15; A6: o <> b by A1, Th7; then A7: Line (o,b) is being_line by Def3; A8: o <> a by A1, Th7; then A9: Line (o,a) is being_line by Def3; A10: a in Line (o,a) by Th15; then A11: a9 in Line (o,a) by A2, A8, A9, A5, Th25; A12: b in Line (o,b) by Th15; A13: o in Line (o,b) by Th15; then A14: b9 in Line (o,b) by A3, A6, A7, A12, Th25; Line (o,a) <> Line (o,b) by A1, A9, A5, A10, A12, Th21; hence ( a9 = o & b9 = o ) by A4, A9, A7, A5, A13, A14, A11, Th18; ::_thesis: verum end; theorem Th55: :: AFF_1:55 for AS being AffinSpace for o, a, b, b9, a9 being Element of AS st not LIN o,a,b & LIN o,b,b9 & a,b // a9,b9 & a9 = o holds b9 = o proof let AS be AffinSpace; ::_thesis: for o, a, b, b9, a9 being Element of AS st not LIN o,a,b & LIN o,b,b9 & a,b // a9,b9 & a9 = o holds b9 = o let o, a, b, b9, a9 be Element of AS; ::_thesis: ( not LIN o,a,b & LIN o,b,b9 & a,b // a9,b9 & a9 = o implies b9 = o ) assume that A1: not LIN o,a,b and A2: LIN o,b,b9 and A3: a,b // a9,b9 and A4: a9 = o ; ::_thesis: b9 = o A5: now__::_thesis:_not_a,b_//_a9,b assume a,b // a9,b ; ::_thesis: contradiction then b,a // b,a9 by Th4; then LIN b,a,a9 by Def1; hence contradiction by A1, A4, Th6; ::_thesis: verum end; a9,b // a9,b9 by A2, A4, Def1; hence b9 = o by A3, A4, A5, Th5; ::_thesis: verum end; theorem :: AFF_1:56 for AS being AffinSpace for o, a, b, a9, b9, x being Element of AS st not LIN o,a,b & LIN o,a,a9 & LIN o,b,b9 & LIN o,b,x & a,b // a9,b9 & a,b // a9,x holds b9 = x proof let AS be AffinSpace; ::_thesis: for o, a, b, a9, b9, x being Element of AS st not LIN o,a,b & LIN o,a,a9 & LIN o,b,b9 & LIN o,b,x & a,b // a9,b9 & a,b // a9,x holds b9 = x let o, a, b, a9, b9, x be Element of AS; ::_thesis: ( not LIN o,a,b & LIN o,a,a9 & LIN o,b,b9 & LIN o,b,x & a,b // a9,b9 & a,b // a9,x implies b9 = x ) assume that A1: not LIN o,a,b and A2: LIN o,a,a9 and A3: LIN o,b,b9 and A4: LIN o,b,x and A5: a,b // a9,b9 and A6: a,b // a9,x ; ::_thesis: b9 = x set A = Line (o,a); set C = Line (o,b); set P = Line (a9,b9); A7: a9 in Line (a9,b9) by Th15; assume A8: b9 <> x ; ::_thesis: contradiction A9: a9 <> b9 proof assume A10: a9 = b9 ; ::_thesis: contradiction then a9 = o by A1, A2, A3, Th54; hence contradiction by A1, A4, A6, A8, A10, Th55; ::_thesis: verum end; then A11: Line (a9,b9) is being_line by Def3; A12: o <> b by A1, Th7; then A13: Line (o,b) is being_line by Def3; A14: b9 in Line (a9,b9) by Th15; a <> b by A1, Th7; then a9,b9 // a9,x by A5, A6, Th5; then LIN a9,b9,x by Def1; then A15: x in Line (a9,b9) by A9, A11, A7, A14, Th25; A16: b in Line (o,b) by Th15; A17: o in Line (o,b) by Th15; then A18: x in Line (o,b) by A4, A12, A13, A16, Th25; b9 in Line (o,b) by A3, A12, A13, A17, A16, Th25; then A19: a9 in Line (o,b) by A8, A13, A11, A7, A14, A18, A15, Th18; A20: o <> a by A1, Th7; then A21: Line (o,a) is being_line by Def3; A22: a9 <> o proof assume A23: a9 = o ; ::_thesis: contradiction then b9 = o by A1, A3, A5, Th55; hence contradiction by A1, A4, A6, A8, A23, Th55; ::_thesis: verum end; A24: o in Line (o,a) by Th15; A25: a in Line (o,a) by Th15; then a9 in Line (o,a) by A2, A20, A21, A24, Th25; then b in Line (o,a) by A22, A21, A13, A24, A17, A16, A19, Th18; hence contradiction by A1, A21, A24, A25, Th21; ::_thesis: verum end; theorem :: AFF_1:57 for AS being AffinSpace for a, b being Element of AS for A being Subset of AS st A is being_line & a in A & b in A & a <> b holds A = Line (a,b) by Lm6; theorem Th58: :: AFF_1:58 for AP being AffinPlane for A, C being Subset of AP st A is being_line & C is being_line & not A // C holds ex x being Element of AP st ( x in A & x in C ) proof let AP be AffinPlane; ::_thesis: for A, C being Subset of AP st A is being_line & C is being_line & not A // C holds ex x being Element of AP st ( x in A & x in C ) let A, C be Subset of AP; ::_thesis: ( A is being_line & C is being_line & not A // C implies ex x being Element of AP st ( x in A & x in C ) ) assume that A1: A is being_line and A2: C is being_line and A3: not A // C ; ::_thesis: ex x being Element of AP st ( x in A & x in C ) consider a, b being Element of AP such that A4: a <> b and A5: A = Line (a,b) by A1, Def3; consider c, d being Element of AP such that A6: c <> d and A7: C = Line (c,d) by A2, Def3; not a,b // c,d by A3, A4, A5, A6, A7, Th37; then consider x being Element of AP such that A8: a,b // a,x and A9: c,d // c,x by DIRAF:46; LIN c,d,x by A9, Def1; then A10: x in C by A7, Def2; LIN a,b,x by A8, Def1; then x in A by A5, Def2; hence ex x being Element of AP st ( x in A & x in C ) by A10; ::_thesis: verum end; theorem :: AFF_1:59 for AP being AffinPlane for a, b being Element of AP for A being Subset of AP st A is being_line & not a,b // A holds ex x being Element of AP st ( x in A & LIN a,b,x ) proof let AP be AffinPlane; ::_thesis: for a, b being Element of AP for A being Subset of AP st A is being_line & not a,b // A holds ex x being Element of AP st ( x in A & LIN a,b,x ) let a, b be Element of AP; ::_thesis: for A being Subset of AP st A is being_line & not a,b // A holds ex x being Element of AP st ( x in A & LIN a,b,x ) let A be Subset of AP; ::_thesis: ( A is being_line & not a,b // A implies ex x being Element of AP st ( x in A & LIN a,b,x ) ) assume that A1: A is being_line and A2: not a,b // A ; ::_thesis: ex x being Element of AP st ( x in A & LIN a,b,x ) set C = Line (a,b); A3: not Line (a,b) // A proof A4: b in Line (a,b) by Th15; assume Line (a,b) // A ; ::_thesis: contradiction then consider p, q being Element of AP such that A5: Line (a,b) = Line (p,q) and A6: p <> q and A7: p,q // A by Def5; a in Line (a,b) by Th15; then p,q // a,b by A5, A6, A4, Th22; hence contradiction by A2, A6, A7, Th32; ::_thesis: verum end; a <> b by A1, A2, Th33; then Line (a,b) is being_line by Def3; then consider x being Element of AP such that A8: x in Line (a,b) and A9: x in A by A1, A3, Th58; LIN a,b,x by A8, Def2; hence ex x being Element of AP st ( x in A & LIN a,b,x ) by A9; ::_thesis: verum end; theorem :: AFF_1:60 for AP being AffinPlane for a, b, c, d being Element of AP st not a,b // c,d holds ex p being Element of AP st ( LIN a,b,p & LIN c,d,p ) proof let AP be AffinPlane; ::_thesis: for a, b, c, d being Element of AP st not a,b // c,d holds ex p being Element of AP st ( LIN a,b,p & LIN c,d,p ) let a, b, c, d be Element of AP; ::_thesis: ( not a,b // c,d implies ex p being Element of AP st ( LIN a,b,p & LIN c,d,p ) ) assume not a,b // c,d ; ::_thesis: ex p being Element of AP st ( LIN a,b,p & LIN c,d,p ) then consider p being Element of AP such that A1: a,b // a,p and A2: c,d // c,p by DIRAF:46; A3: LIN c,d,p by A2, Def1; LIN a,b,p by A1, Def1; hence ex p being Element of AP st ( LIN a,b,p & LIN c,d,p ) by A3; ::_thesis: verum end;