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 ) )

thus ( P = Q implies ( A on Q & L on Q ) ) by A2, A3, A8, Def14, Th9; :: thesis: verum

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

A8:
{B,C} \/ {A} on P
by A4, ENUMSET1:3;
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;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

thus ( P = Q implies ( A on Q & L on Q ) ) by A2, A3, A8, Def14, Th9; :: thesis: verum