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