let S be IncSpace; :: thesis: for C, A, B 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 C, A, B 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, Th35;
C on Plane C,L by A1, Def21;
then {A,B} \/ {C} on Plane C,L by A4, Th19;
then A5: {A,B,C} on Plane C,L by ENUMSET1:43;
not {A,B,C} is linear by A1, A2, A3, Th39;
hence Plane C,L = Plane A,B,C by A5, Def20; :: thesis: verum