let AS be AffinSpace; :: thesis: for a, b being POINT of (IncProjSp_of AS)
for A, K being LINE of (IncProjSp_of AS) st a on A & a on K & b on A & b on K & not a = b holds
A = K
let a, b be POINT of (IncProjSp_of AS); :: thesis: for A, K being LINE of (IncProjSp_of AS) st a on A & a on K & b on A & b on K & not a = b holds
A = K
let A, K be LINE of (IncProjSp_of AS); :: thesis: ( a on A & a on K & b on A & b on K & not a = b implies A = K )
assume that
A1: a on A and
A2: a on K and
A3: b on A and
A4: b on K ; :: thesis: ( a = b or A = K )
consider X being Subset of AS such that
A5: ( ( A = [X,1] & X is being_line ) or ( A = [(PDir X),2] & X is being_plane ) ) by Th23;
consider X9 being Subset of AS such that
A6: ( ( K = [X9,1] & X9 is being_line ) or ( K = [(PDir X9),2] & X9 is being_plane ) ) by Th23;
assume A7: a <> b ; :: thesis: A = K

A8: now :: thesis: ( ex Y being Subset of AS st
( a = LDir Y & Y is being_line ) implies A = K )

given Y being Subset of AS such that A9: a = LDir Y and
A10: Y is being_line ; :: thesis: A = K

A11: now :: thesis: ( ex Y9 being Subset of AS st
( b = LDir Y9 & Y9 is being_line ) implies A = K )

given Y9 being Subset of AS such that A12: b = LDir Y9 and
A13: Y9 is being_line ; :: thesis: A = K
A14: not Y // Y9 by A7, A9, A10, A12, A13, Th11;
A15: for Z being Subset of AS
for M being LINE of (IncProjSp_of AS) st M = [Z,1] & Z is being_line & a on M holds
not b on M

proof

let Z be Subset of AS; :: thesis: for M being LINE of (IncProjSp_of AS) st M = [Z,1] & Z is being_line & a on M holds
not b on M
let M be LINE of (IncProjSp_of AS); :: thesis: ( M = [Z,1] & Z is being_line & a on M implies not b on M )
assume that
A16: M = [Z,1] and
A17: Z is being_line ; :: thesis: ( not a on M or not b on M )
assume A18: ( a on M & b on M ) ; :: thesis: contradiction
then Y9 '||' Z by A12, A13, A16, A17, Th28;
then A19: Y9 // Z by A13, A17, AFF_4:40;
Y '||' Z by A9, A10, A16, A17, A18, Th28;
then Y // Z by A10, A17, AFF_4:40;
then Y // Y9 by A19, AFF_1:44;
hence contradiction by A7, A9, A10, A12, A13, Th11; :: thesis: verum

end;

then A20: Y9 '||' X by A1, A3, A5, A12, A13, Th29;
A21: Y9 '||' X9 by A2, A4, A6, A12, A13, A15, Th29;
A22: Y '||' X9 by A2, A4, A6, A9, A10, A15, Th29;
Y '||' X by A1, A3, A5, A9, A10, A15, Th29;
then X '||' X9 by A1, A2, A3, A4, A5, A6, A10, A13, A15, A14, A22, A20, A21, Th5;
hence A = K by A1, A2, A3, A4, A5, A6, A15, Th13; :: thesis: verum

end;

now :: thesis: ( b is Element of AS implies A = K )

assume b is Element of AS ; :: thesis: A = K
then reconsider y = b as Element of AS ;
A23: y in X9 by A4, A6, Th26, Th27;
A24: y = b ;
then Y '||' X9 by A2, A4, A6, A9, A10, Th27, Th28;
then A25: Y // X9 by A4, A6, A10, A24, Th27, AFF_4:40;
Y '||' X by A1, A3, A5, A9, A10, A24, Th27, Th28;
then Y // X by A3, A5, A10, A24, Th27, AFF_4:40;
then A26: X // X9 by A25, AFF_1:44;
y in X by A3, A5, Th26, Th27;
hence A = K by A3, A4, A5, A6, A23, A26, Th27, AFF_1:45; :: thesis: verum

end;

hence A = K by A11, Th20; :: thesis: verum

end;

now :: thesis: ( a is Element of AS implies A = K )

assume a is Element of AS ; :: thesis: A = K
then reconsider x = a as Element of AS ;
A27: x = a ;
A28: x in X9 by A2, A6, Th26, Th27;
A29: x in X by A1, A5, Th26, Th27;

A30: now :: thesis: ( ex Y being Subset of AS st
( b = LDir Y & Y is being_line ) implies A = K )

given Y being Subset of AS such that A31: b = LDir Y and
A32: Y is being_line ; :: thesis: A = K
Y '||' X9 by A2, A4, A6, A27, A31, A32, Th27, Th28;
then A33: Y // X9 by A2, A6, A27, A32, Th27, AFF_4:40;
Y '||' X by A1, A3, A5, A27, A31, A32, Th27, Th28;
then Y // X by A1, A5, A27, A32, Th27, AFF_4:40;
then X // X9 by A33, AFF_1:44;
hence A = K by A1, A2, A5, A6, A29, A28, Th27, AFF_1:45; :: thesis: verum

end;

now :: thesis: ( b is Element of AS implies A = K )

assume b is Element of AS ; :: thesis: A = K
then reconsider y = b as Element of AS ;
A34: y in X9 by A4, A6, Th26, Th27;
y in X by A3, A5, Th26, Th27;
hence A = K by A1, A2, A7, A5, A6, A29, A28, A34, Th27, AFF_1:18; :: thesis: verum

end;

hence A = K by A30, Th20; :: thesis: verum

end;

hence A = K by A8, Th20; :: thesis: verum