:: COLLSP semantic presentation begin definition let X be set ; mode Relation3 of X -> set means :Def1: :: COLLSP:def 1 it c= [:X,X,X:]; existence ex b1 being set st b1 c= [:X,X,X:] ; end; :: deftheorem Def1 defines Relation3 COLLSP:def_1_:_ for X, b2 being set holds ( b2 is Relation3 of X iff b2 c= [:X,X,X:] ); theorem Th1: :: COLLSP:1 for X being set holds ( X = {} or ex a being set st ( {a} = X or ex a, b being set st ( a <> b & a in X & b in X ) ) ) proof let X be set ; ::_thesis: ( X = {} or ex a being set st ( {a} = X or ex a, b being set st ( a <> b & a in X & b in X ) ) ) now__::_thesis:_(_X_<>_{}_&_(_for_a,_b_being_set_holds_ (_not_a_<>_b_or_not_a_in_X_or_not_b_in_X_)_)_implies_ex_a_being_set_st_{a}_=_X_) set p = the Element of X; assume ( X <> {} & ( for a, b being set holds ( not a <> b or not a in X or not b in X ) ) ) ; ::_thesis: ex a being set st {a} = X then for z being set holds ( z in X iff z = the Element of X ) ; then X = { the Element of X} by TARSKI:def_1; hence ex a being set st {a} = X ; ::_thesis: verum end; hence ( X = {} or ex a being set st ( {a} = X or ex a, b being set st ( a <> b & a in X & b in X ) ) ) ; ::_thesis: verum end; definition attrc1 is strict ; struct CollStr -> 1-sorted ; aggrCollStr(# carrier, Collinearity #) -> CollStr ; sel Collinearity c1 -> Relation3 of the carrier of c1; end; registration cluster non empty strict for CollStr ; existence ex b1 being CollStr st ( not b1 is empty & b1 is strict ) proof set A = the non empty set ; set r = the Relation3 of the non empty set ; take CollStr(# the non empty set , the Relation3 of the non empty set #) ; ::_thesis: ( not CollStr(# the non empty set , the Relation3 of the non empty set #) is empty & CollStr(# the non empty set , the Relation3 of the non empty set #) is strict ) thus not the carrier of CollStr(# the non empty set , the Relation3 of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: CollStr(# the non empty set , the Relation3 of the non empty set #) is strict thus CollStr(# the non empty set , the Relation3 of the non empty set #) is strict ; ::_thesis: verum end; end; definition let CS be non empty CollStr ; let a, b, c be Point of CS; preda,b,c is_collinear means :Def2: :: COLLSP:def 2 [a,b,c] in the Collinearity of CS; end; :: deftheorem Def2 defines is_collinear COLLSP:def_2_:_ for CS being non empty CollStr for a, b, c being Point of CS holds ( a,b,c is_collinear iff [a,b,c] in the Collinearity of CS ); set Z = {1}; Lm1: 1 in {1} by TARSKI:def_1; Lm2: {[1,1,1]} c= [:{1},{1},{1}:] proof now__::_thesis:_for_x_being_set_st_x_in_{[1,1,1]}_holds_ x_in_[:{1},{1},{1}:] let x be set ; ::_thesis: ( x in {[1,1,1]} implies x in [:{1},{1},{1}:] ) assume x in {[1,1,1]} ; ::_thesis: x in [:{1},{1},{1}:] then x = [1,1,1] by TARSKI:def_1; hence x in [:{1},{1},{1}:] by Lm1, MCART_1:69; ::_thesis: verum end; hence {[1,1,1]} c= [:{1},{1},{1}:] by TARSKI:def_3; ::_thesis: verum end; reconsider Z = {1} as non empty set ; reconsider RR = {[1,1,1]} as Relation3 of Z by Def1, Lm2; reconsider CLS = CollStr(# Z,RR #) as non empty CollStr ; Lm3: now__::_thesis:_for_a,_b,_c,_p,_q,_r_being_Point_of_CLS_holds_ (_(_(_a_=_b_or_a_=_c_or_b_=_c_)_implies_[a,b,c]_in_the_Collinearity_of_CLS_)_&_(_a_<>_b_&_[a,b,p]_in_the_Collinearity_of_CLS_&_[a,b,q]_in_the_Collinearity_of_CLS_&_[a,b,r]_in_the_Collinearity_of_CLS_implies_[p,q,r]_in_the_Collinearity_of_CLS_)_) let a, b, c, p, q, r be Point of CLS; ::_thesis: ( ( ( a = b or a = c or b = c ) implies [a,b,c] in the Collinearity of CLS ) & ( a <> b & [a,b,p] in the Collinearity of CLS & [a,b,q] in the Collinearity of CLS & [a,b,r] in the Collinearity of CLS implies [p,q,r] in the Collinearity of CLS ) ) A1: for z1, z2, z3 being Point of CLS holds [z1,z2,z3] in the Collinearity of CLS proof let z1, z2, z3 be Point of CLS; ::_thesis: [z1,z2,z3] in the Collinearity of CLS A2: z3 = 1 by TARSKI:def_1; ( z1 = 1 & z2 = 1 ) by TARSKI:def_1; hence [z1,z2,z3] in the Collinearity of CLS by A2, TARSKI:def_1; ::_thesis: verum end; hence ( ( a = b or a = c or b = c ) implies [a,b,c] in the Collinearity of CLS ) ; ::_thesis: ( a <> b & [a,b,p] in the Collinearity of CLS & [a,b,q] in the Collinearity of CLS & [a,b,r] in the Collinearity of CLS implies [p,q,r] in the Collinearity of CLS ) thus ( a <> b & [a,b,p] in the Collinearity of CLS & [a,b,q] in the Collinearity of CLS & [a,b,r] in the Collinearity of CLS implies [p,q,r] in the Collinearity of CLS ) by A1; ::_thesis: verum end; definition let IT be non empty CollStr ; attrIT is reflexive means :Def3: :: COLLSP:def 3 for a, b, c being Point of IT st ( a = b or a = c or b = c ) holds [a,b,c] in the Collinearity of IT; end; :: deftheorem Def3 defines reflexive COLLSP:def_3_:_ for IT being non empty CollStr holds ( IT is reflexive iff for a, b, c being Point of IT st ( a = b or a = c or b = c ) holds [a,b,c] in the Collinearity of IT ); definition let IT be non empty CollStr ; attrIT is transitive means :Def4: :: COLLSP:def 4 for a, b, p, q, r being Point of IT st a <> b & [a,b,p] in the Collinearity of IT & [a,b,q] in the Collinearity of IT & [a,b,r] in the Collinearity of IT holds [p,q,r] in the Collinearity of IT; end; :: deftheorem Def4 defines transitive COLLSP:def_4_:_ for IT being non empty CollStr holds ( IT is transitive iff for a, b, p, q, r being Point of IT st a <> b & [a,b,p] in the Collinearity of IT & [a,b,q] in the Collinearity of IT & [a,b,r] in the Collinearity of IT holds [p,q,r] in the Collinearity of IT ); registration cluster non empty strict reflexive transitive for CollStr ; existence ex b1 being non empty CollStr st ( b1 is strict & b1 is reflexive & b1 is transitive ) proof take CLS ; ::_thesis: ( CLS is strict & CLS is reflexive & CLS is transitive ) thus ( CLS is strict & CLS is reflexive & CLS is transitive ) by Def3, Def4, Lm3; ::_thesis: verum end; end; definition mode CollSp is non empty reflexive transitive CollStr ; end; theorem Th2: :: COLLSP:2 for CLSP being CollSp for a, b, c being Point of CLSP st ( a = b or a = c or b = c ) holds a,b,c is_collinear proof let CLSP be CollSp; ::_thesis: for a, b, c being Point of CLSP st ( a = b or a = c or b = c ) holds a,b,c is_collinear let a, b, c be Point of CLSP; ::_thesis: ( ( a = b or a = c or b = c ) implies a,b,c is_collinear ) assume ( a = b or a = c or b = c ) ; ::_thesis: a,b,c is_collinear then [a,b,c] in the Collinearity of CLSP by Def3; hence a,b,c is_collinear by Def2; ::_thesis: verum end; theorem Th3: :: COLLSP:3 for CLSP being CollSp for a, b, p, q, r being Point of CLSP st a <> b & a,b,p is_collinear & a,b,q is_collinear & a,b,r is_collinear holds p,q,r is_collinear proof let CLSP be CollSp; ::_thesis: for a, b, p, q, r being Point of CLSP st a <> b & a,b,p is_collinear & a,b,q is_collinear & a,b,r is_collinear holds p,q,r is_collinear let a, b, p, q, r be Point of CLSP; ::_thesis: ( a <> b & a,b,p is_collinear & a,b,q is_collinear & a,b,r is_collinear implies p,q,r is_collinear ) assume that A1: a <> b and A2: ( a,b,p is_collinear & a,b,q is_collinear ) and A3: a,b,r is_collinear ; ::_thesis: p,q,r is_collinear A4: [a,b,r] in the Collinearity of CLSP by A3, Def2; ( [a,b,p] in the Collinearity of CLSP & [a,b,q] in the Collinearity of CLSP ) by A2, Def2; then [p,q,r] in the Collinearity of CLSP by A1, A4, Def4; hence p,q,r is_collinear by Def2; ::_thesis: verum end; theorem Th4: :: COLLSP:4 for CLSP being CollSp for a, b, c being Point of CLSP st a,b,c is_collinear holds ( b,a,c is_collinear & a,c,b is_collinear ) proof let CLSP be CollSp; ::_thesis: for a, b, c being Point of CLSP st a,b,c is_collinear holds ( b,a,c is_collinear & a,c,b is_collinear ) let a, b, c be Point of CLSP; ::_thesis: ( a,b,c is_collinear implies ( b,a,c is_collinear & a,c,b is_collinear ) ) assume A1: a,b,c is_collinear ; ::_thesis: ( b,a,c is_collinear & a,c,b is_collinear ) then ( a = b or ( a <> b & a,b,b is_collinear & a,b,a is_collinear & a,b,c is_collinear ) ) by Th2; hence b,a,c is_collinear by Th2, Th3; ::_thesis: a,c,b is_collinear ( a = b or ( a <> b & a,b,a is_collinear & a,b,c is_collinear & a,b,b is_collinear ) ) by A1, Th2; hence a,c,b is_collinear by Th2, Th3; ::_thesis: verum end; theorem :: COLLSP:5 for CLSP being CollSp for a, b being Point of CLSP holds a,b,a is_collinear by Th2; theorem Th6: :: COLLSP:6 for CLSP being CollSp for a, b, c, d being Point of CLSP st a <> b & a,b,c is_collinear & a,b,d is_collinear holds a,c,d is_collinear proof let CLSP be CollSp; ::_thesis: for a, b, c, d being Point of CLSP st a <> b & a,b,c is_collinear & a,b,d is_collinear holds a,c,d is_collinear let a, b, c, d be Point of CLSP; ::_thesis: ( a <> b & a,b,c is_collinear & a,b,d is_collinear implies a,c,d is_collinear ) assume A1: ( a <> b & a,b,c is_collinear & a,b,d is_collinear ) ; ::_thesis: a,c,d is_collinear a,b,a is_collinear by Th2; hence a,c,d is_collinear by A1, Th3; ::_thesis: verum end; theorem :: COLLSP:7 for CLSP being CollSp for a, b, c being Point of CLSP st a,b,c is_collinear holds b,a,c is_collinear by Th4; theorem Th8: :: COLLSP:8 for CLSP being CollSp for a, b, c being Point of CLSP st a,b,c is_collinear holds b,c,a is_collinear proof let CLSP be CollSp; ::_thesis: for a, b, c being Point of CLSP st a,b,c is_collinear holds b,c,a is_collinear let a, b, c be Point of CLSP; ::_thesis: ( a,b,c is_collinear implies b,c,a is_collinear ) assume a,b,c is_collinear ; ::_thesis: b,c,a is_collinear then b,a,c is_collinear by Th4; hence b,c,a is_collinear by Th4; ::_thesis: verum end; theorem Th9: :: COLLSP:9 for CLSP being CollSp for p, q, a, b, r being Point of CLSP st p <> q & a,b,p is_collinear & a,b,q is_collinear & p,q,r is_collinear holds a,b,r is_collinear proof let CLSP be CollSp; ::_thesis: for p, q, a, b, r being Point of CLSP st p <> q & a,b,p is_collinear & a,b,q is_collinear & p,q,r is_collinear holds a,b,r is_collinear let p, q, a, b, r be Point of CLSP; ::_thesis: ( p <> q & a,b,p is_collinear & a,b,q is_collinear & p,q,r is_collinear implies a,b,r is_collinear ) assume that A1: p <> q and A2: ( a,b,p is_collinear & a,b,q is_collinear ) and A3: p,q,r is_collinear ; ::_thesis: a,b,r is_collinear now__::_thesis:_(_a_<>_b_implies_a,b,r_is_collinear_) assume A4: a <> b ; ::_thesis: a,b,r is_collinear then a,p,q is_collinear by A2, Th6; then A5: p,q,a is_collinear by Th8; a,b,b is_collinear by Th2; then p,q,b is_collinear by A2, A4, Th3; hence a,b,r is_collinear by A1, A3, A5, Th3; ::_thesis: verum end; hence a,b,r is_collinear by Th2; ::_thesis: verum end; definition let CLSP be CollSp; let a, b be Point of CLSP; func Line (a,b) -> set equals :: COLLSP:def 5 { p where p is Point of CLSP : a,b,p is_collinear } ; correctness coherence { p where p is Point of CLSP : a,b,p is_collinear } is set ; ; end; :: deftheorem defines Line COLLSP:def_5_:_ for CLSP being CollSp for a, b being Point of CLSP holds Line (a,b) = { p where p is Point of CLSP : a,b,p is_collinear } ; theorem Th10: :: COLLSP:10 for CLSP being CollSp for a, b being Point of CLSP holds ( a in Line (a,b) & b in Line (a,b) ) proof let CLSP be CollSp; ::_thesis: for a, b being Point of CLSP holds ( a in Line (a,b) & b in Line (a,b) ) let a, b be Point of CLSP; ::_thesis: ( a in Line (a,b) & b in Line (a,b) ) a,b,a is_collinear by Th2; hence a in Line (a,b) ; ::_thesis: b in Line (a,b) a,b,b is_collinear by Th2; hence b in Line (a,b) ; ::_thesis: verum end; theorem Th11: :: COLLSP:11 for CLSP being CollSp for a, b, r being Point of CLSP holds ( a,b,r is_collinear iff r in Line (a,b) ) proof let CLSP be CollSp; ::_thesis: for a, b, r being Point of CLSP holds ( a,b,r is_collinear iff r in Line (a,b) ) let a, b, r be Point of CLSP; ::_thesis: ( a,b,r is_collinear iff r in Line (a,b) ) thus ( a,b,r is_collinear implies r in Line (a,b) ) ; ::_thesis: ( r in Line (a,b) implies a,b,r is_collinear ) thus ( r in Line (a,b) implies a,b,r is_collinear ) ::_thesis: verum proof assume r in Line (a,b) ; ::_thesis: a,b,r is_collinear then ex p being Point of CLSP st ( r = p & a,b,p is_collinear ) ; hence a,b,r is_collinear ; ::_thesis: verum end; end; set Z = {1,2,3}; set RR = { [i,j,k] where i, j, k is Element of NAT : ( ( i = j or j = k or k = i ) & i in {1,2,3} & j in {1,2,3} & k in {1,2,3} ) } ; Lm4: { [i,j,k] where i, j, k is Element of NAT : ( ( i = j or j = k or k = i ) & i in {1,2,3} & j in {1,2,3} & k in {1,2,3} ) } c= [:{1,2,3},{1,2,3},{1,2,3}:] proof now__::_thesis:_for_x_being_set_st_x_in__{__[i,j,k]_where_i,_j,_k_is_Element_of_NAT_:_(_(_i_=_j_or_j_=_k_or_k_=_i_)_&_i_in_{1,2,3}_&_j_in_{1,2,3}_&_k_in_{1,2,3}_)__}__holds_ x_in_[:{1,2,3},{1,2,3},{1,2,3}:] let x be set ; ::_thesis: ( x in { [i,j,k] where i, j, k is Element of NAT : ( ( i = j or j = k or k = i ) & i in {1,2,3} & j in {1,2,3} & k in {1,2,3} ) } implies x in [:{1,2,3},{1,2,3},{1,2,3}:] ) assume x in { [i,j,k] where i, j, k is Element of NAT : ( ( i = j or j = k or k = i ) & i in {1,2,3} & j in {1,2,3} & k in {1,2,3} ) } ; ::_thesis: x in [:{1,2,3},{1,2,3},{1,2,3}:] then ex i, j, k being Element of NAT st ( x = [i,j,k] & ( i = j or j = k or k = i ) & i in {1,2,3} & j in {1,2,3} & k in {1,2,3} ) ; hence x in [:{1,2,3},{1,2,3},{1,2,3}:] by MCART_1:69; ::_thesis: verum end; hence { [i,j,k] where i, j, k is Element of NAT : ( ( i = j or j = k or k = i ) & i in {1,2,3} & j in {1,2,3} & k in {1,2,3} ) } c= [:{1,2,3},{1,2,3},{1,2,3}:] by TARSKI:def_3; ::_thesis: verum end; reconsider Z = {1,2,3} as non empty set by ENUMSET1:def_1; reconsider RR = { [i,j,k] where i, j, k is Element of NAT : ( ( i = j or j = k or k = i ) & i in {1,2,3} & j in {1,2,3} & k in {1,2,3} ) } as Relation3 of Z by Def1, Lm4; reconsider CLS = CollStr(# Z,RR #) as non empty CollStr ; Lm5: for a, b, c being Point of CLS holds ( [a,b,c] in RR iff ( ( a = b or b = c or c = a ) & a in Z & b in Z & c in Z ) ) proof let a, b, c be Point of CLS; ::_thesis: ( [a,b,c] in RR iff ( ( a = b or b = c or c = a ) & a in Z & b in Z & c in Z ) ) thus ( [a,b,c] in RR implies ( ( a = b or b = c or c = a ) & a in Z & b in Z & c in Z ) ) ::_thesis: ( ( a = b or b = c or c = a ) & a in Z & b in Z & c in Z implies [a,b,c] in RR ) proof assume [a,b,c] in RR ; ::_thesis: ( ( a = b or b = c or c = a ) & a in Z & b in Z & c in Z ) then consider i, j, k being Element of NAT such that A1: [a,b,c] = [i,j,k] and A2: ( i = j or j = k or k = i ) and i in Z and j in Z and k in Z ; ( a = i & b = j ) by A1, XTUPLE_0:3; hence ( ( a = b or b = c or c = a ) & a in Z & b in Z & c in Z ) by A1, A2, XTUPLE_0:3; ::_thesis: verum end; thus ( ( a = b or b = c or c = a ) & a in Z & b in Z & c in Z implies [a,b,c] in RR ) ; ::_thesis: verum end; Lm6: for a, b, c, p, q, r being Point of CLS st a <> b & [a,b,p] in the Collinearity of CLS & [a,b,q] in the Collinearity of CLS & [a,b,r] in the Collinearity of CLS holds [p,q,r] in the Collinearity of CLS proof let a, b, c, p, q, r be Point of CLS; ::_thesis: ( a <> b & [a,b,p] in the Collinearity of CLS & [a,b,q] in the Collinearity of CLS & [a,b,r] in the Collinearity of CLS implies [p,q,r] in the Collinearity of CLS ) assume that A1: a <> b and A2: [a,b,p] in the Collinearity of CLS and A3: [a,b,q] in the Collinearity of CLS and A4: [a,b,r] in the Collinearity of CLS ; ::_thesis: [p,q,r] in the Collinearity of CLS A5: ( a = q or b = q ) by A1, A3, Lm5; A6: ( a = r or b = r ) by A1, A4, Lm5; A7: ( p in Z & q in Z ) ; A8: r in Z ; ( a = p or b = p ) by A1, A2, Lm5; hence [p,q,r] in the Collinearity of CLS by A5, A6, A7, A8; ::_thesis: verum end; Lm7: not for a, b, c being Point of CLS holds a,b,c is_collinear proof reconsider a = 1, b = 2, c = 3 as Point of CLS by ENUMSET1:def_1; take a ; ::_thesis: not for b, c being Point of CLS holds a,b,c is_collinear take b ; ::_thesis: not for c being Point of CLS holds a,b,c is_collinear take c ; ::_thesis: not a,b,c is_collinear not [a,b,c] in the Collinearity of CLS by Lm5; hence not a,b,c is_collinear by Def2; ::_thesis: verum end; Lm8: CLS is CollSp proof for a, b, c, p, q, r being Point of CLS holds ( ( ( a = b or a = c or b = c ) implies [a,b,c] in the Collinearity of CLS ) & ( a <> b & [a,b,p] in the Collinearity of CLS & [a,b,q] in the Collinearity of CLS & [a,b,r] in the Collinearity of CLS implies [p,q,r] in the Collinearity of CLS ) ) by Lm5, Lm6; hence CLS is CollSp by Def3, Def4; ::_thesis: verum end; definition let IT be non empty CollStr ; attrIT is proper means :Def6: :: COLLSP:def 6 not for a, b, c being Point of IT holds a,b,c is_collinear ; end; :: deftheorem Def6 defines proper COLLSP:def_6_:_ for IT being non empty CollStr holds ( IT is proper iff not for a, b, c being Point of IT holds a,b,c is_collinear ); registration cluster non empty strict reflexive transitive proper for CollStr ; existence ex b1 being CollSp st ( b1 is strict & b1 is proper ) proof reconsider CLS = CLS as CollSp by Lm8; CLS is proper by Def6, Lm7; hence ex b1 being CollSp st ( b1 is strict & b1 is proper ) ; ::_thesis: verum end; end; theorem Th12: :: COLLSP:12 for CLSP being proper CollSp for p, q being Point of CLSP st p <> q holds ex r being Point of CLSP st not p,q,r is_collinear proof let CLSP be proper CollSp; ::_thesis: for p, q being Point of CLSP st p <> q holds ex r being Point of CLSP st not p,q,r is_collinear let p, q be Point of CLSP; ::_thesis: ( p <> q implies ex r being Point of CLSP st not p,q,r is_collinear ) consider a, b, c being Point of CLSP such that A1: not a,b,c is_collinear by Def6; assume p <> q ; ::_thesis: not for r being Point of CLSP holds p,q,r is_collinear then ( not p,q,a is_collinear or not p,q,b is_collinear or not p,q,c is_collinear ) by A1, Th3; hence not for r being Point of CLSP holds p,q,r is_collinear ; ::_thesis: verum end; definition let CLSP be proper CollSp; mode LINE of CLSP -> set means :Def7: :: COLLSP:def 7 ex a, b being Point of CLSP st ( a <> b & it = Line (a,b) ); existence ex b1 being set ex a, b being Point of CLSP st ( a <> b & b1 = Line (a,b) ) proof consider a, b, c being Point of CLSP such that A1: not a,b,c is_collinear by Def6; take Line (a,b) ; ::_thesis: ex a, b being Point of CLSP st ( a <> b & Line (a,b) = Line (a,b) ) a <> b by A1, Th2; hence ex a, b being Point of CLSP st ( a <> b & Line (a,b) = Line (a,b) ) ; ::_thesis: verum end; end; :: deftheorem Def7 defines LINE COLLSP:def_7_:_ for CLSP being proper CollSp for b2 being set holds ( b2 is LINE of CLSP iff ex a, b being Point of CLSP st ( a <> b & b2 = Line (a,b) ) ); theorem :: COLLSP:13 for CLSP being proper CollSp for a, b being Point of CLSP st a = b holds Line (a,b) = the carrier of CLSP proof let CLSP be proper CollSp; ::_thesis: for a, b being Point of CLSP st a = b holds Line (a,b) = the carrier of CLSP let a, b be Point of CLSP; ::_thesis: ( a = b implies Line (a,b) = the carrier of CLSP ) assume A1: a = b ; ::_thesis: Line (a,b) = the carrier of CLSP for x being set holds ( x in Line (a,b) iff x in the carrier of CLSP ) proof let x be set ; ::_thesis: ( x in Line (a,b) iff x in the carrier of CLSP ) thus ( x in Line (a,b) implies x in the carrier of CLSP ) ::_thesis: ( x in the carrier of CLSP implies x in Line (a,b) ) proof assume x in Line (a,b) ; ::_thesis: x in the carrier of CLSP then ex p being Point of CLSP st ( x = p & a,b,p is_collinear ) ; then reconsider x = x as Point of CLSP ; x is Element of CLSP ; hence x in the carrier of CLSP ; ::_thesis: verum end; thus ( x in the carrier of CLSP implies x in Line (a,b) ) ::_thesis: verum proof assume x in the carrier of CLSP ; ::_thesis: x in Line (a,b) then reconsider x = x as Point of CLSP ; a,b,x is_collinear by A1, Th2; hence x in Line (a,b) ; ::_thesis: verum end; end; hence Line (a,b) = the carrier of CLSP by TARSKI:1; ::_thesis: verum end; theorem :: COLLSP:14 for CLSP being proper CollSp for P being LINE of CLSP ex a, b being Point of CLSP st ( a <> b & a in P & b in P ) proof let CLSP be proper CollSp; ::_thesis: for P being LINE of CLSP ex a, b being Point of CLSP st ( a <> b & a in P & b in P ) let P be LINE of CLSP; ::_thesis: ex a, b being Point of CLSP st ( a <> b & a in P & b in P ) consider a, b being Point of CLSP such that A1: ( a <> b & P = Line (a,b) ) by Def7; take a ; ::_thesis: ex b being Point of CLSP st ( a <> b & a in P & b in P ) take b ; ::_thesis: ( a <> b & a in P & b in P ) thus ( a <> b & a in P & b in P ) by A1, Th10; ::_thesis: verum end; theorem :: COLLSP:15 for CLSP being proper CollSp for a, b being Point of CLSP st a <> b holds ex P being LINE of CLSP st ( a in P & b in P ) proof let CLSP be proper CollSp; ::_thesis: for a, b being Point of CLSP st a <> b holds ex P being LINE of CLSP st ( a in P & b in P ) let a, b be Point of CLSP; ::_thesis: ( a <> b implies ex P being LINE of CLSP st ( a in P & b in P ) ) assume a <> b ; ::_thesis: ex P being LINE of CLSP st ( a in P & b in P ) then reconsider P = Line (a,b) as LINE of CLSP by Def7; take P ; ::_thesis: ( a in P & b in P ) thus ( a in P & b in P ) by Th10; ::_thesis: verum end; theorem Th16: :: COLLSP:16 for CLSP being proper CollSp for p, q, r being Point of CLSP for P being LINE of CLSP st p in P & q in P & r in P holds p,q,r is_collinear proof let CLSP be proper CollSp; ::_thesis: for p, q, r being Point of CLSP for P being LINE of CLSP st p in P & q in P & r in P holds p,q,r is_collinear let p, q, r be Point of CLSP; ::_thesis: for P being LINE of CLSP st p in P & q in P & r in P holds p,q,r is_collinear let P be LINE of CLSP; ::_thesis: ( p in P & q in P & r in P implies p,q,r is_collinear ) assume that A1: ( p in P & q in P ) and A2: r in P ; ::_thesis: p,q,r is_collinear consider a, b being Point of CLSP such that A3: a <> b and A4: P = Line (a,b) by Def7; A5: ex z being Point of CLSP st ( z = r & a,b,z is_collinear ) by A2, A4; ( ex x being Point of CLSP st ( x = p & a,b,x is_collinear ) & ex y being Point of CLSP st ( y = q & a,b,y is_collinear ) ) by A1, A4; hence p,q,r is_collinear by A3, A5, Th3; ::_thesis: verum end; Lm9: for CLSP being proper CollSp for P being LINE of CLSP for x being set st x in P holds x is Point of CLSP proof let CLSP be proper CollSp; ::_thesis: for P being LINE of CLSP for x being set st x in P holds x is Point of CLSP let P be LINE of CLSP; ::_thesis: for x being set st x in P holds x is Point of CLSP let x be set ; ::_thesis: ( x in P implies x is Point of CLSP ) consider a, b being Point of CLSP such that a <> b and A1: P = Line (a,b) by Def7; assume x in P ; ::_thesis: x is Point of CLSP then ex r being Point of CLSP st ( r = x & a,b,r is_collinear ) by A1; hence x is Point of CLSP ; ::_thesis: verum end; theorem Th17: :: COLLSP:17 for CLSP being proper CollSp for P, Q being LINE of CLSP st P c= Q holds P = Q proof let CLSP be proper CollSp; ::_thesis: for P, Q being LINE of CLSP st P c= Q holds P = Q let P, Q be LINE of CLSP; ::_thesis: ( P c= Q implies P = Q ) assume A1: P c= Q ; ::_thesis: P = Q Q c= P proof let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in Q or r in P ) consider p, q being Point of CLSP such that p <> q and A2: P = Line (p,q) by Def7; assume A3: r in Q ; ::_thesis: r in P then reconsider r = r as Point of CLSP by Lm9; ( p in P & q in P ) by A2, Th10; then p,q,r is_collinear by A1, A3, Th16; hence r in P by A2; ::_thesis: verum end; hence P = Q by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th18: :: COLLSP:18 for CLSP being proper CollSp for p, q being Point of CLSP for P being LINE of CLSP st p <> q & p in P & q in P holds Line (p,q) c= P proof let CLSP be proper CollSp; ::_thesis: for p, q being Point of CLSP for P being LINE of CLSP st p <> q & p in P & q in P holds Line (p,q) c= P let p, q be Point of CLSP; ::_thesis: for P being LINE of CLSP st p <> q & p in P & q in P holds Line (p,q) c= P let P be LINE of CLSP; ::_thesis: ( p <> q & p in P & q in P implies Line (p,q) c= P ) assume that A1: p <> q and A2: ( p in P & q in P ) ; ::_thesis: Line (p,q) c= P let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Line (p,q) or x in P ) consider a, b being Point of CLSP such that a <> b and A3: P = Line (a,b) by Def7; assume x in Line (p,q) ; ::_thesis: x in P then consider r being Point of CLSP such that A4: r = x and A5: p,q,r is_collinear ; ( a,b,p is_collinear & a,b,q is_collinear ) by A2, A3, Th11; then a,b,r is_collinear by A1, A5, Th9; hence x in P by A3, A4; ::_thesis: verum end; theorem Th19: :: COLLSP:19 for CLSP being proper CollSp for p, q being Point of CLSP for P being LINE of CLSP st p <> q & p in P & q in P holds Line (p,q) = P proof let CLSP be proper CollSp; ::_thesis: for p, q being Point of CLSP for P being LINE of CLSP st p <> q & p in P & q in P holds Line (p,q) = P let p, q be Point of CLSP; ::_thesis: for P being LINE of CLSP st p <> q & p in P & q in P holds Line (p,q) = P let P be LINE of CLSP; ::_thesis: ( p <> q & p in P & q in P implies Line (p,q) = P ) assume that A1: p <> q and A2: ( p in P & q in P ) ; ::_thesis: Line (p,q) = P reconsider Q = Line (p,q) as LINE of CLSP by A1, Def7; Q c= P by A1, A2, Th18; hence Line (p,q) = P by Th17; ::_thesis: verum end; theorem Th20: :: COLLSP:20 for CLSP being proper CollSp for p, q being Point of CLSP for P, Q being LINE of CLSP st p <> q & p in P & q in P & p in Q & q in Q holds P = Q proof let CLSP be proper CollSp; ::_thesis: for p, q being Point of CLSP for P, Q being LINE of CLSP st p <> q & p in P & q in P & p in Q & q in Q holds P = Q let p, q be Point of CLSP; ::_thesis: for P, Q being LINE of CLSP st p <> q & p in P & q in P & p in Q & q in Q holds P = Q let P, Q be LINE of CLSP; ::_thesis: ( p <> q & p in P & q in P & p in Q & q in Q implies P = Q ) assume that A1: p <> q and A2: ( p in P & q in P ) and A3: ( p in Q & q in Q ) ; ::_thesis: P = Q Line (p,q) = P by A1, A2, Th19; hence P = Q by A1, A3, Th19; ::_thesis: verum end; theorem :: COLLSP:21 for CLSP being proper CollSp for P, Q being LINE of CLSP holds ( P = Q or P misses Q or ex p being Point of CLSP st P /\ Q = {p} ) proof let CLSP be proper CollSp; ::_thesis: for P, Q being LINE of CLSP holds ( P = Q or P misses Q or ex p being Point of CLSP st P /\ Q = {p} ) let P, Q be LINE of CLSP; ::_thesis: ( P = Q or P misses Q or ex p being Point of CLSP st P /\ Q = {p} ) A1: ( ex a being set st {a} = P /\ Q implies ex p being Point of CLSP st P /\ Q = {p} ) proof given a being set such that A2: {a} = P /\ Q ; ::_thesis: ex p being Point of CLSP st P /\ Q = {p} a in P /\ Q by A2, TARSKI:def_1; then a in P by XBOOLE_0:def_4; then reconsider p = a as Point of CLSP by Lm9; P /\ Q = {p} by A2; hence ex p being Point of CLSP st P /\ Q = {p} ; ::_thesis: verum end; A3: ( ex a, b being set st ( a <> b & a in P /\ Q & b in P /\ Q ) implies P = Q ) proof given a, b being set such that A4: a <> b and A5: ( a in P /\ Q & b in P /\ Q ) ; ::_thesis: P = Q ( a in P & b in P ) by A5, XBOOLE_0:def_4; then reconsider p = a, q = b as Point of CLSP by Lm9; A6: ( p in Q & q in Q ) by A5, XBOOLE_0:def_4; ( p in P & q in P ) by A5, XBOOLE_0:def_4; hence P = Q by A4, A6, Th20; ::_thesis: verum end; ( P /\ Q = {} or ex a being set st ( {a} = P /\ Q or ex a, b being set st ( a <> b & a in P /\ Q & b in P /\ Q ) ) ) by Th1; hence ( P = Q or P misses Q or ex p being Point of CLSP st P /\ Q = {p} ) by A1, A3, XBOOLE_0:def_7; ::_thesis: verum end; theorem :: COLLSP:22 for CLSP being proper CollSp for a, b being Point of CLSP st a <> b holds Line (a,b) <> the carrier of CLSP proof let CLSP be proper CollSp; ::_thesis: for a, b being Point of CLSP st a <> b holds Line (a,b) <> the carrier of CLSP let a, b be Point of CLSP; ::_thesis: ( a <> b implies Line (a,b) <> the carrier of CLSP ) assume a <> b ; ::_thesis: Line (a,b) <> the carrier of CLSP then not for r being Point of CLSP holds a,b,r is_collinear by Th12; hence Line (a,b) <> the carrier of CLSP by Th11; ::_thesis: verum end;