let S be IncSpace; for P, Q being PLANE of S holds
( not P <> Q or for A being POINT of S holds
( not A on P or not A on Q ) or ex L being LINE of S st
for B being POINT of S holds
( ( B on P & B on Q ) iff B on L ) )
let P, Q be PLANE of S; ( not P <> Q or for A being POINT of S holds
( not A on P or not A on Q ) or ex L being LINE of S st
for B being POINT of S holds
( ( B on P & B on Q ) iff B on L ) )
assume A1:
P <> Q
; ( for A being POINT of S holds
( not A on P or not A on Q ) or ex L being LINE of S st
for B being POINT of S holds
( ( B on P & B on Q ) iff B on L ) )
given A being POINT of S such that A2:
A on P
and
A3:
A on Q
; ex L being LINE of S st
for B being POINT of S holds
( ( B on P & B on Q ) iff B on L )
consider C being POINT of S such that
A4:
A <> C
and
A5:
C on P
and
A6:
C on Q
by A2, A3, Def15;
take L = Line (A,C); for B being POINT of S holds
( ( B on P & B on Q ) iff B on L )
A7:
{A,C} on L
by A4, Def19;
{A,C} on Q
by A3, A6, Th3;
then A8:
L on Q
by A4, A7, Def14;
let B be POINT of S; ( ( B on P & B on Q ) iff B on L )
{A,C} on P
by A2, A5, Th3;
then A9:
L on P
by A4, A7, Def14;
thus
( B on P & B on Q implies B on L )
( B on L implies ( B on P & B on Q ) )proof
assume that A10:
B on P
and A11:
B on Q
and A12:
not
B on L
;
contradiction
consider P1 being
PLANE of
S such that A13:
for
P2 being
PLANE of
S holds
( (
B on P2 &
L on P2 ) iff
P1 = P2 )
by A12, Th26;
P = P1
by A9, A10, A13;
hence
contradiction
by A1, A8, A11, A13;
verum
end;
thus
( B on L implies ( B on P & B on Q ) )
by A9, A8, Def17; verum