:: 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;