let AS be AffinSpace; :: thesis: for a, b being POINT of
for A, K being LINE of 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 ; :: thesis: for A, K being LINE of 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 ; :: 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 such that
A5: ( ( A = [X,1] & X is being_line ) or ( A = [(PDir X),2] & X is being_plane ) ) by Th23;
consider X' being Subset of such that
A6: ( ( K = [X',1] & X' is being_line ) or ( K = [(PDir X'),2] & X' is being_plane ) ) by Th23;
assume A7: a <> b ; :: thesis: A = K

A8: now

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

A11: now

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

proof

let Z be Subset of ; :: thesis: for M being LINE of st M = [Z,1] & Z is being_line & a on M holds
not b on M
let M be LINE of ; :: 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 Y' '||' Z by A12, A13, A16, A17, Th28;
then A19: Y' // 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 // Y' by A19, AFF_1:58;
hence contradiction by A7, A9, A10, A12, A13, Th11; :: thesis: verum

end;

then A20: Y' '||' X by A1, A3, A5, A12, A13, Th29;
A21: Y' '||' X' by A2, A4, A6, A12, A13, A15, Th29;
A22: Y '||' X' by A2, A4, A6, A9, A10, A15, Th29;
Y '||' X by A1, A3, A5, A9, A10, A15, Th29;
then X '||' X' 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

assume b is Element of ; :: thesis: A = K
then reconsider y = b as Element of ;
A23: y in X' by A4, A6, Th26, Th27;
A24: y = b ;
then Y '||' X' by A2, A4, A6, A9, A10, Th27, Th28;
then A25: Y // X' 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 // X' by A25, AFF_1:58;
y in X by A3, A5, Th26, Th27;
hence A = K by A3, A4, A5, A6, A23, A26, Th27, AFF_1:59; :: thesis: verum

end;

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

end;

now

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

A30: now

given Y being Subset of such that A31: b = LDir Y and
A32: Y is being_line ; :: thesis: A = K
Y '||' X' by A2, A4, A6, A27, A31, A32, Th27, Th28;
then A33: Y // X' 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 // X' by A33, AFF_1:58;
hence A = K by A1, A2, A5, A6, A29, A28, Th27, AFF_1:59; :: thesis: verum

end;

now

assume b is Element of ; :: thesis: A = K
then reconsider y = b as Element of ;
A34: y in X' 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:30; :: thesis: verum

end;

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

end;

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