let S be IncSpace; :: thesis: for A, B, C being POINT of S st not {A,B,C} is linear holds

ex P being PLANE of S st

for Q being PLANE of S holds

( {A,B,C} on Q iff P = Q )

let A, B, C be POINT of S; :: thesis: ( not {A,B,C} is linear implies ex P being PLANE of S st

for Q being PLANE of S holds

( {A,B,C} on Q iff P = Q ) )

assume A1: not {A,B,C} is linear ; :: thesis: ex P being PLANE of S st

for Q being PLANE of S holds

( {A,B,C} on Q iff P = Q )

consider P being PLANE of S such that

A2: {A,B,C} on P by Def12;

take P ; :: thesis: for Q being PLANE of S holds

( {A,B,C} on Q iff P = Q )

thus for Q being PLANE of S holds

( {A,B,C} on Q iff P = Q ) by A1, A2, Def13; :: thesis: verum

ex P being PLANE of S st

for Q being PLANE of S holds

( {A,B,C} on Q iff P = Q )

let A, B, C be POINT of S; :: thesis: ( not {A,B,C} is linear implies ex P being PLANE of S st

for Q being PLANE of S holds

( {A,B,C} on Q iff P = Q ) )

assume A1: not {A,B,C} is linear ; :: thesis: ex P being PLANE of S st

for Q being PLANE of S holds

( {A,B,C} on Q iff P = Q )

consider P being PLANE of S such that

A2: {A,B,C} on P by Def12;

take P ; :: thesis: for Q being PLANE of S holds

( {A,B,C} on Q iff P = Q )

thus for Q being PLANE of S holds

( {A,B,C} on Q iff P = Q ) by A1, A2, Def13; :: thesis: verum