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

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