let S be IncSpace; :: thesis: for A being POINT of S
for L being LINE of S st not A on L holds
ex P being PLANE of S st
for Q being PLANE of S holds
( ( A on Q & L on Q ) iff P = Q )
let A be POINT of S; :: thesis: for L being LINE of S st not A on L holds
ex P being PLANE of S st
for Q being PLANE of S holds
( ( A on Q & L on Q ) iff P = Q )
let L be LINE of S; :: thesis: ( not A on L implies ex P being PLANE of S st
for Q being PLANE of S holds
( ( A on Q & L on Q ) iff P = Q ) )
assume A1: not A on L ; :: thesis: ex P being PLANE of S st
for Q being PLANE of S holds
( ( A on Q & L on Q ) iff P = Q )
consider B, C being POINT of S such that
A2: B <> C and
A3: {B,C} on L by Def8;
consider P being PLANE of S such that
A4: {B,C,A} on P by Def12;
take P ; :: thesis: for Q being PLANE of S holds
( ( A on Q & L on Q ) iff P = Q )
let Q be PLANE of S; :: thesis: ( ( A on Q & L on Q ) iff P = Q )
thus ( A on Q & L on Q implies P = Q ) :: thesis: ( P = Q implies ( A on Q & L on Q ) )

proof

assume that
A5: A on Q and
A6: L on Q ; :: thesis: P = Q
{B,C} on Q by A3, A6, Th14;
then ( B on Q & C on Q ) by Th3;
then A7: {B,C,A} on Q by A5, Th4;
not {B,C,A} is linear by A1, A2, A3, Th18;
hence P = Q by A4, A7, Def13; :: thesis: verum

end;

A8: {B,C} \/ {A} on P by A4, ENUMSET1:3;
thus ( P = Q implies ( A on Q & L on Q ) ) by A2, A3, A8, Def14, Th9; :: thesis: verum