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;
( C on Plane C,L & L on Plane C,L ) by A1, Def21;
then ( C on Plane C,L & {A,B} on Plane C,L ) by A2, Th35;
then {A,B} \/ {C} on Plane C,L by Th19;
then A4: {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 A4, Def20; :: thesis: verum