let S be IncSpace; :: thesis: for A, B, C being POINT of S

for L being LINE of S st not C on L & {A,B} on L & A <> B holds

Plane (C,L) = Plane (A,B,C)

let A, B, C be POINT of S; :: thesis: for L being LINE of S st not C on L & {A,B} on L & A <> B holds

Plane (C,L) = Plane (A,B,C)

let L be LINE of S; :: thesis: ( not C on L & {A,B} on L & A <> B implies Plane (C,L) = Plane (A,B,C) )

assume that

A1: not C on L and

A2: {A,B} on L and

A3: A <> B ; :: thesis: Plane (C,L) = Plane (A,B,C)

set P1 = Plane (C,L);

L on Plane (C,L) by A1, Def21;

then A4: {A,B} on Plane (C,L) by A2, Th14;

C on Plane (C,L) by A1, Def21;

then {A,B} \/ {C} on Plane (C,L) by A4, Th9;

then A5: {A,B,C} on Plane (C,L) by ENUMSET1:3;

not {A,B,C} is linear by A1, A2, A3, Th18;

hence Plane (C,L) = Plane (A,B,C) by A5, Def20; :: thesis: verum

for L being LINE of S st not C on L & {A,B} on L & A <> B holds

Plane (C,L) = Plane (A,B,C)

let A, B, C be POINT of S; :: thesis: for L being LINE of S st not C on L & {A,B} on L & A <> B holds

Plane (C,L) = Plane (A,B,C)

let L be LINE of S; :: thesis: ( not C on L & {A,B} on L & A <> B implies Plane (C,L) = Plane (A,B,C) )

assume that

A1: not C on L and

A2: {A,B} on L and

A3: A <> B ; :: thesis: Plane (C,L) = Plane (A,B,C)

set P1 = Plane (C,L);

L on Plane (C,L) by A1, Def21;

then A4: {A,B} on Plane (C,L) by A2, Th14;

C on Plane (C,L) by A1, Def21;

then {A,B} \/ {C} on Plane (C,L) by A4, Th9;

then A5: {A,B,C} on Plane (C,L) by ENUMSET1:3;

not {A,B,C} is linear by A1, A2, A3, Th18;

hence Plane (C,L) = Plane (A,B,C) by A5, Def20; :: thesis: verum