consider B, C being POINT of S such that
A2: ( B <> C & {B,C} on L ) by Def8;
consider P being PLANE of S such that
A3: {B,C,A} on P by Def12;
take P ; :: thesis: ( A on P & L on P )
thus A on P by A3, Th4; :: thesis: L on P
{B,C} \/ {A} on P by A3, ENUMSET1:3;
then {B,C} on P by Th9;
hence L on P by A2, Def14; :: thesis: verum