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