let S be IncSpace; 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; 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; ( 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
; 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
; for Q being PLANE of S holds
( ( A on Q & L on Q ) iff P = Q )
let Q be PLANE of S; ( ( A on Q & L on Q ) iff P = Q )
thus
( A on Q & L on Q implies P = Q )
( P = Q implies ( A on Q & L on Q ) )proof
assume that A5:
A on Q
and A6:
L on Q
;
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;
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; verum