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

A c= C by A1, A2, A3, A4;

hence A = C by A15, XBOOLE_0:def 10; :: thesis: verum

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

then A15:
C c= A
by A1, A2, A3;
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, Th35;

A9: A is being_line by A5;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in C )

assume A10: x in A ; :: thesis: x in C

then reconsider x9 = x as Element of AS ;

end;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, Th35;

A9: A is being_line by A5;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or 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 )

hence
x in C
by A7; :: thesis: verumconsider q being Element of AS such that

A11: p <> q and

A12: q in C by A8, Th19;

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, Th28, Th42;

then p,x9 // p,q by A7, A8, A11, A12, Th26;

then p,q // p,x9 by Th3;

then A14: LIN p,q,x9 ;

C = Line (p,q) by A7, A8, A11, A12, Lm6;

hence x in C by A14, Def2; :: thesis: verum

end;A11: p <> q and

A12: q in C by A8, Th19;

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, Th28, Th42;

then p,x9 // p,q by A7, A8, A11, A12, Th26;

then p,q // p,x9 by Th3;

then A14: LIN p,q,x9 ;

C = Line (p,q) by A7, A8, A11, A12, Lm6;

hence x in C by A14, Def2; :: thesis: verum

A c= C by A1, A2, A3, A4;

hence A = C by A15, XBOOLE_0:def 10; :: thesis: verum