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 A2, A3, Def15;

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 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; :: 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 A4, A7, Def14;

thus ( B on P & B on Q implies B on L ) :: thesis: ( B on L implies ( B on P & B on Q ) )

( 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 A2, A3, Def15;

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 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; :: 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 A4, A7, Def14;

thus ( B on P & B on Q implies B on L ) :: thesis: ( B on L implies ( B on P & B on Q ) )

proof

thus
( B on L implies ( B on P & B on Q ) )
by A9, A8, Def17; :: thesis: verum
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 A12, Th26;

P = P1 by A9, A10, A13;

hence contradiction by A1, A8, A11, A13; :: thesis: verum

end;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 A12, Th26;

P = P1 by A9, A10, A13;

hence contradiction by A1, A8, A11, A13; :: thesis: verum