let S be IncSpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: 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 ;
take L = Line (A,C); :: thesis: for B being POINT of S holds
( ( B on P & B on Q ) iff B on L )

A7: {A,C} on L by ;
{A,C} on Q by A3, A6, Th3;
then A8: L on Q by ;
let B be POINT of S; :: thesis: ( ( B on P & B on Q ) iff B on L )
{A,C} on P by A2, A5, Th3;
then A9: L on P by ;
thus ( B on P & B on Q implies B on L ) :: thesis: ( 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 ; :: thesis: 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 ;
P = P1 by A9, A10, A13;
hence contradiction by A1, A8, A11, A13; :: thesis: verum
end;
thus ( B on L implies ( B on P & B on Q ) ) by ; :: thesis: verum