:: Axioms of Incidence
:: by Wojciech A. Trybulec
::
:: Received April 14, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users

definition

attr c₁ is strict ;
struct IncProjStr -> ;
aggr IncProjStr(# Points, Lines, Inc #) -> IncProjStr ;
sel Points c₁ -> non empty set ;
sel Lines c₁ -> non empty set ;
sel Inc c₁ -> Relation of the Points of c₁, the Lines of c₁;

end;

definition

attr c₁ is strict ;
struct IncStruct -> IncProjStr ;
aggr IncStruct(# Points, Lines, Planes, Inc, Inc2, Inc3 #) -> IncStruct ;
sel Planes c₁ -> non empty set ;
sel Inc2 c₁ -> Relation of the Points of c₁, the Planes of c₁;
sel Inc3 c₁ -> Relation of the Lines of c₁, the Planes of c₁;

end;

definition

let S be IncProjStr ;
mode POINT of S is Element of the Points of S;
mode LINE of S is Element of the Lines of S;

end;

definition

let S be IncStruct ;
mode PLANE of S is Element of the Planes of S;

end;

:: Definitions of predicates 'on' and attributes 'linear', 'planar'

definition

let S be IncProjStr ;
let A be POINT of S;
let L be LINE of S;

pred A on L means :: INCSP_1:def 1
[A,L] in the Inc of S;

end;

:: deftheorem defines on INCSP_1:def 1 :
for S being IncProjStr
for A being POINT of S
for L being LINE of S holds
( A on L iff [A,L] in the Inc of S );

definition

let S be IncStruct ;
let A be POINT of S;
let P be PLANE of S;

pred A on P means :: INCSP_1:def 2
[A,P] in the Inc2 of S;

end;

:: deftheorem defines on INCSP_1:def 2 :
for S being IncStruct
for A being POINT of S
for P being PLANE of S holds
( A on P iff [A,P] in the Inc2 of S );

definition

let S be IncStruct ;
let L be LINE of S;
let P be PLANE of S;

pred L on P means :: INCSP_1:def 3
[L,P] in the Inc3 of S;

end;

:: deftheorem defines on INCSP_1:def 3 :
for S being IncStruct
for L being LINE of S
for P being PLANE of S holds
( L on P iff [L,P] in the Inc3 of S );

definition

let S be IncProjStr ;
let F be Subset of the Points of S;
let L be LINE of S;

pred F on L means :: INCSP_1:def 4
for A being POINT of S st A in F holds
A on L;

end;

:: deftheorem defines on INCSP_1:def 4 :
for S being IncProjStr
for F being Subset of the Points of S
for L being LINE of S holds
( F on L iff for A being POINT of S st A in F holds
A on L );

definition

let S be IncStruct ;
let F be Subset of the Points of S;
let P be PLANE of S;

pred F on P means :: INCSP_1:def 5
for A being POINT of S st A in F holds
A on P;

end;

:: deftheorem defines on INCSP_1:def 5 :
for S being IncStruct
for F being Subset of the Points of S
for P being PLANE of S holds
( F on P iff for A being POINT of S st A in F holds
A on P );

definition

let S be IncProjStr ;
let F be Subset of the Points of S;

attr F is linear means :: INCSP_1:def 6
ex L being LINE of S st F on L;

end;

:: deftheorem defines linear INCSP_1:def 6 :
for S being IncProjStr
for F being Subset of the Points of S holds
( F is linear iff ex L being LINE of S st F on L );

definition

let S be IncStruct ;
let F be Subset of the Points of S;

attr F is planar means :: INCSP_1:def 7
ex P being PLANE of S st F on P;

end;

:: deftheorem defines planar INCSP_1:def 7 :
for S being IncStruct
for F being Subset of the Points of S holds
( F is planar iff ex P being PLANE of S st F on P );

theorem Th1: :: INCSP_1:1

for S being IncProjStr
for L being LINE of S
for A, B being POINT of S holds
( {A,B} on L iff ( A on L & B on L ) )

proof end;

theorem Th2: :: INCSP_1:2

for S being IncProjStr
for L being LINE of S
for A, B, C being POINT of S holds
( {A,B,C} on L iff ( A on L & B on L & C on L ) )

proof end;

theorem Th3: :: INCSP_1:3

for S being IncStruct
for A, B being POINT of S
for P being PLANE of S holds
( {A,B} on P iff ( A on P & B on P ) )

proof end;

theorem Th4: :: INCSP_1:4

for S being IncStruct
for A, B, C being POINT of S
for P being PLANE of S holds
( {A,B,C} on P iff ( A on P & B on P & C on P ) )

proof end;

theorem Th5: :: INCSP_1:5

for S being IncStruct
for A, B, C, D being POINT of S
for P being PLANE of S holds
( {A,B,C,D} on P iff ( A on P & B on P & C on P & D on P ) )

proof end;

theorem Th6: :: INCSP_1:6

for S being IncStruct
for L being LINE of S
for F, G being Subset of the Points of S st G c= F & F on L holds
G on L ;

theorem Th7: :: INCSP_1:7

for S being IncStruct
for P being PLANE of S
for F, G being Subset of the Points of S st G c= F & F on P holds
G on P ;

theorem Th8: :: INCSP_1:8

for S being IncStruct
for A being POINT of S
for L being LINE of S
for F being Subset of the Points of S holds
( ( F on L & A on L ) iff F \/ {A} on L )

proof end;

theorem Th9: :: INCSP_1:9

for S being IncStruct
for A being POINT of S
for P being PLANE of S
for F being Subset of the Points of S holds
( ( F on P & A on P ) iff F \/ {A} on P )

proof end;

theorem Th10: :: INCSP_1:10

for S being IncStruct
for L being LINE of S
for F, G being Subset of the Points of S holds
( F \/ G on L iff ( F on L & G on L ) )

proof end;

theorem Th11: :: INCSP_1:11

for S being IncStruct
for P being PLANE of S
for F, G being Subset of the Points of S holds
( F \/ G on P iff ( F on P & G on P ) )

proof end;

theorem :: INCSP_1:12

for S being IncStruct
for F, G being Subset of the Points of S st G c= F & F is linear holds
G is linear

proof end;

theorem :: INCSP_1:13

for S being IncStruct
for F, G being Subset of the Points of S st G c= F & F is planar holds
G is planar

proof end;

:: Introduction of mode IncSpace

definition

let S be IncProjStr ;

attr S is with_non-trivial_lines means :Def8: :: INCSP_1:def 8
for L being LINE of S ex A, B being POINT of S st
( A <> B & {A,B} on L );

attr S is linear means :Def9: :: INCSP_1:def 9
for A, B being POINT of S ex L being LINE of S st {A,B} on L;

attr S is up-2-rank means :Def10: :: INCSP_1:def 10
for A, B being POINT of S
for K, L being LINE of S st A <> B & {A,B} on K & {A,B} on L holds
K = L;

end;

:: deftheorem Def8 defines with_non-trivial_lines INCSP_1:def 8 :
for S being IncProjStr holds
( S is with_non-trivial_lines iff for L being LINE of S ex A, B being POINT of S st
( A <> B & {A,B} on L ) );

:: deftheorem Def9 defines linear INCSP_1:def 9 :
for S being IncProjStr holds
( S is linear iff for A, B being POINT of S ex L being LINE of S st {A,B} on L );

:: deftheorem Def10 defines up-2-rank INCSP_1:def 10 :
for S being IncProjStr holds
( S is up-2-rank iff for A, B being POINT of S
for K, L being LINE of S st A <> B & {A,B} on K & {A,B} on L holds
K = L );

definition

let S be IncStruct ;

attr S is with_non-empty_planes means :Def11: :: INCSP_1:def 11
for P being PLANE of S ex A being POINT of S st A on P;

attr S is planar means :Def12: :: INCSP_1:def 12
for A, B, C being POINT of S ex P being PLANE of S st {A,B,C} on P;

attr S is with_<=1_plane_per_3_pts means :Def13: :: INCSP_1:def 13
for A, B, C being POINT of S
for P, Q being PLANE of S st not {A,B,C} is linear & {A,B,C} on P & {A,B,C} on Q holds
P = Q;

attr S is with_lines_inside_planes means :Def14: :: INCSP_1:def 14
for L being LINE of S
for P being PLANE of S st ex A, B being POINT of S st
( A <> B & {A,B} on L & {A,B} on P ) holds
L on P;

attr S is with_planes_intersecting_in_2_pts means :Def15: :: INCSP_1:def 15
for A being POINT of S
for P, Q being PLANE of S st A on P & A on Q holds
ex B being POINT of S st
( A <> B & B on P & B on Q );

attr S is up-3-dimensional means :Def16: :: INCSP_1:def 16
not for A, B, C, D being POINT of S holds {A,B,C,D} is planar ;

attr S is inc-compatible means :Def17: :: INCSP_1:def 17
for A being POINT of S
for L being LINE of S
for P being PLANE of S st A on L & L on P holds
A on P;

end;

:: deftheorem Def11 defines with_non-empty_planes INCSP_1:def 11 :
for S being IncStruct holds
( S is with_non-empty_planes iff for P being PLANE of S ex A being POINT of S st A on P );

:: deftheorem Def12 defines planar INCSP_1:def 12 :
for S being IncStruct holds
( S is planar iff for A, B, C being POINT of S ex P being PLANE of S st {A,B,C} on P );

:: deftheorem Def13 defines with_<=1_plane_per_3_pts INCSP_1:def 13 :
for S being IncStruct holds
( S is with_<=1_plane_per_3_pts iff for A, B, C being POINT of S
for P, Q being PLANE of S st not {A,B,C} is linear & {A,B,C} on P & {A,B,C} on Q holds
P = Q );

:: deftheorem Def14 defines with_lines_inside_planes INCSP_1:def 14 :
for S being IncStruct holds
( S is with_lines_inside_planes iff for L being LINE of S
for P being PLANE of S st ex A, B being POINT of S st
( A <> B & {A,B} on L & {A,B} on P ) holds
L on P );

:: deftheorem Def15 defines with_planes_intersecting_in_2_pts INCSP_1:def 15 :
for S being IncStruct holds
( S is with_planes_intersecting_in_2_pts iff for A being POINT of S
for P, Q being PLANE of S st A on P & A on Q holds
ex B being POINT of S st
( A <> B & B on P & B on Q ) );

:: deftheorem Def16 defines up-3-dimensional INCSP_1:def 16 :
for S being IncStruct holds
( S is up-3-dimensional iff not for A, B, C, D being POINT of S holds {A,B,C,D} is planar );

:: deftheorem Def17 defines inc-compatible INCSP_1:def 17 :
for S being IncStruct holds
( S is inc-compatible iff for A being POINT of S
for L being LINE of S
for P being PLANE of S st A on L & L on P holds
A on P );

definition

let IT be IncStruct ;

attr IT is IncSpace-like means :: INCSP_1:def 18
( IT is with_non-trivial_lines & IT is linear & IT is up-2-rank & IT is with_non-empty_planes & IT is planar & IT is with_<=1_plane_per_3_pts & IT is with_lines_inside_planes & IT is with_planes_intersecting_in_2_pts & IT is up-3-dimensional & IT is inc-compatible );

end;

:: deftheorem defines IncSpace-like INCSP_1:def 18 :
for IT being IncStruct holds
( IT is IncSpace-like iff ( IT is with_non-trivial_lines & IT is linear & IT is up-2-rank & IT is with_non-empty_planes & IT is planar & IT is with_<=1_plane_per_3_pts & IT is with_lines_inside_planes & IT is with_planes_intersecting_in_2_pts & IT is up-3-dimensional & IT is inc-compatible ) );

registration

cluster IncSpace-like -> with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible for IncStruct ;

coherence
for b₁ being IncStruct st b₁ is IncSpace-like holds
( b₁ is with_non-trivial_lines & b₁ is linear & b₁ is up-2-rank & b₁ is with_non-empty_planes & b₁ is planar & b₁ is with_<=1_plane_per_3_pts & b₁ is with_lines_inside_planes & b₁ is with_planes_intersecting_in_2_pts & b₁ is up-3-dimensional & b₁ is inc-compatible ) ;

end;

registration

cluster strict IncSpace-like for IncStruct ;

existence
ex b₁ being IncStruct st
( b₁ is strict & b₁ is IncSpace-like )

proof end;

end;

definition

mode IncSpace is IncSpace-like IncStruct ;

end;

:: Axioms of Incidence

theorem Th14: :: INCSP_1:14

for S being IncSpace
for L being LINE of S
for P being PLANE of S
for F being Subset of the Points of S st F on L & L on P holds
F on P by Def17;

:: Collinearity of points & coplanarity of points & lines

theorem Th15: :: INCSP_1:15

for S being IncSpace
for A, B being POINT of S holds {A,A,B} is linear

proof end;

theorem Th16: :: INCSP_1:16

for S being IncSpace
for A, B, C being POINT of S holds {A,A,B,C} is planar

proof end;

theorem Th17: :: INCSP_1:17

for S being IncSpace
for A, B, C, D being POINT of S st {A,B,C} is linear holds
{A,B,C,D} is planar

proof end;

theorem Th18: :: INCSP_1:18

for S being IncSpace
for A, B, C being POINT of S
for L being LINE of S st A <> B & {A,B} on L & not C on L holds
not {A,B,C} is linear

proof end;

theorem Th19: :: INCSP_1:19

for S being IncSpace
for A, B, C, D being POINT of S
for P being PLANE of S st not {A,B,C} is linear & {A,B,C} on P & not D on P holds
not {A,B,C,D} is planar

proof end;

theorem :: INCSP_1:20

for S being IncSpace
for K, L being LINE of S st ( for P being PLANE of S holds
( not K on P or not L on P ) ) holds
K <> L

proof end;

Lm1: for S being IncSpace
for A being POINT of S
for L being LINE of S ex B being POINT of S st
( A <> B & B on L )

proof end;

theorem :: INCSP_1:21

for S being IncSpace
for L, L1, L2 being LINE of S st ( for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ) & ex A being POINT of S st
( A on L & A on L1 & A on L2 ) holds
L <> L1

proof end;

theorem :: INCSP_1:22

for S being IncSpace
for L, L1, L2 being LINE of S
for P being PLANE of S st L1 on P & L2 on P & not L on P & L1 <> L2 holds
for Q being PLANE of S holds
( not L on Q or not L1 on Q or not L2 on Q )

proof end;

:: Lines & planes

theorem Th23: :: INCSP_1:23

for S being IncSpace
for K, L being LINE of S st ex A being POINT of S st
( A on K & A on L ) holds
ex P being PLANE of S st
( K on P & L on P )

proof end;

theorem :: INCSP_1:24

for S being IncSpace
for A, B being POINT of S st A <> B holds
ex L being LINE of S st
for K being LINE of S holds
( {A,B} on K iff K = L )

proof end;

theorem :: INCSP_1:25

for S being IncSpace
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 )

proof end;

theorem Th26: :: INCSP_1:26

for S being 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 )

proof end;

theorem Th27: :: INCSP_1:27

for S being IncSpace
for K, L being LINE of S st K <> L & ex A being POINT of S st
( A on K & A on L ) holds
ex P being PLANE of S st
for Q being PLANE of S holds
( ( K on Q & L on Q ) iff P = Q )

proof end;

:: Definitions of functions: Line, Plane

definition

let S be IncSpace;
let A, B be POINT of S;
assume A1: A <> B ;

func Line (A,B) -> LINE of S means :Def19: :: INCSP_1:def 19
{A,B} on it;

correctness
existence
ex b₁ being LINE of S st {A,B} on b₁;
uniqueness
for b₁, b₂ being LINE of S st {A,B} on b₁ & {A,B} on b₂ holds
b₁ = b₂;
by A1, Def9, Def10;

end;

:: deftheorem Def19 defines Line INCSP_1:def 19 :
for S being IncSpace
for A, B being POINT of S st A <> B holds
for b₄ being LINE of S holds
( b₄ = Line (A,B) iff {A,B} on b₄ );

definition

let S be IncSpace;
let A, B, C be POINT of S;
assume A1: not {A,B,C} is linear ;

func Plane (A,B,C) -> PLANE of S means :Def20: :: INCSP_1:def 20
{A,B,C} on it;

correctness
existence
ex b₁ being PLANE of S st {A,B,C} on b₁;
uniqueness
for b₁, b₂ being PLANE of S st {A,B,C} on b₁ & {A,B,C} on b₂ holds
b₁ = b₂;
by A1, Def12, Def13;

end;

:: deftheorem Def20 defines Plane INCSP_1:def 20 :
for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
for b₅ being PLANE of S holds
( b₅ = Plane (A,B,C) iff {A,B,C} on b₅ );

definition

let S be IncSpace;
let A be POINT of S;
let L be LINE of S;
assume A1: not A on L ;

func Plane (A,L) -> PLANE of S means :Def21: :: INCSP_1:def 21
( A on it & L on it );

existence
ex b₁ being PLANE of S st
( A on b₁ & L on b₁ )

proof end;

uniqueness
for b₁, b₂ being PLANE of S st A on b₁ & L on b₁ & A on b₂ & L on b₂ holds
b₁ = b₂

proof end;

end;

:: deftheorem Def21 defines Plane INCSP_1:def 21 :
for S being IncSpace
for A being POINT of S
for L being LINE of S st not A on L holds
for b₄ being PLANE of S holds
( b₄ = Plane (A,L) iff ( A on b₄ & L on b₄ ) );

definition

let S be IncSpace;
let K, L be LINE of S;
assume that
A1: K <> L and
A2: ex A being POINT of S st
( A on K & A on L ) ;

func Plane (K,L) -> PLANE of S means :Def22: :: INCSP_1:def 22
( K on it & L on it );

existence
ex b₁ being PLANE of S st
( K on b₁ & L on b₁ ) by A2, Th23;
uniqueness
for b₁, b₂ being PLANE of S st K on b₁ & L on b₁ & K on b₂ & L on b₂ holds
b₁ = b₂

proof end;

end;

:: deftheorem Def22 defines Plane INCSP_1:def 22 :
for S being IncSpace
for K, L being LINE of S st K <> L & ex A being POINT of S st
( A on K & A on L ) holds
for b₄ being PLANE of S holds
( b₄ = Plane (K,L) iff ( K on b₄ & L on b₄ ) );

:: Definitional theorems of functions: Line, Plane

theorem :: INCSP_1:28

for S being IncSpace
for A, B being POINT of S st A <> B holds
Line (A,B) = Line (B,A)

proof end;

theorem Th29: :: INCSP_1:29

for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (A,C,B)

proof end;

theorem Th30: :: INCSP_1:30

for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (B,A,C)

proof end;

theorem :: INCSP_1:31

for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (B,C,A)

proof end;

theorem Th32: :: INCSP_1:32

for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (C,A,B)

proof end;

theorem :: INCSP_1:33

for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (C,B,A)

proof end;

theorem :: INCSP_1:34

for S being IncSpace
for K, L being LINE of S st K <> L & ex A being POINT of S st
( A on K & A on L ) holds
Plane (K,L) = Plane (L,K)

proof end;

theorem Th35: :: INCSP_1:35

for S being IncSpace
for A, B, C being POINT of S st A <> B & C on Line (A,B) holds
{A,B,C} is linear

proof end;

theorem :: INCSP_1:36

for S being IncSpace
for A, B, C being POINT of S st A <> B & A <> C & {A,B,C} is linear holds
Line (A,B) = Line (A,C)

proof end;

theorem :: INCSP_1:37

for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane (C,(Line (A,B)))

proof end;

theorem :: INCSP_1:38

for S being IncSpace
for A, B, C, D being POINT of S st not {A,B,C} is linear & D on Plane (A,B,C) holds
{A,B,C,D} is planar

proof end;

theorem :: INCSP_1:39

for S being IncSpace
for A, B, C being POINT of S
for L being LINE of S st not C on L & {A,B} on L & A <> B holds
Plane (C,L) = Plane (A,B,C)

proof end;

theorem :: INCSP_1:40

for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane (A,B,C) = Plane ((Line (A,B)),(Line (A,C)))

proof end;

Lm2: for S being IncSpace
for P being PLANE of S ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar )

proof end;

:: The fourth axiom of incidence

theorem Th41: :: INCSP_1:41

for S being IncSpace
for P being PLANE of S ex A, B, C being POINT of S st
( {A,B,C} on P & not {A,B,C} is linear )

proof end;

:: Fundamental existence theorems

theorem :: INCSP_1:42

for S being IncSpace
for P being PLANE of S ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar ) by Lm2;

theorem :: INCSP_1:43

for S being IncSpace
for A being POINT of S
for L being LINE of S ex B being POINT of S st
( A <> B & B on L ) by Lm1;

theorem Th44: :: INCSP_1:44

for S being IncSpace
for A, B being POINT of S
for P being PLANE of S st A <> B holds
ex C being POINT of S st
( C on P & not {A,B,C} is linear )

proof end;

theorem Th45: :: INCSP_1:45

for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
ex D being POINT of S st not {A,B,C,D} is planar

proof end;

theorem Th46: :: INCSP_1:46

for S being IncSpace
for A being POINT of S
for P being PLANE of S ex B, C being POINT of S st
( {B,C} on P & not {A,B,C} is linear )

proof end;

theorem Th47: :: INCSP_1:47

for S being IncSpace
for A, B being POINT of S st A <> B holds
ex C, D being POINT of S st not {A,B,C,D} is planar

proof end;

theorem :: INCSP_1:48

for S being IncSpace
for A being POINT of S holds
not for B, C, D being POINT of S holds {A,B,C,D} is planar

proof end;

theorem :: INCSP_1:49

for S being IncSpace
for A being POINT of S
for P being PLANE of S ex L being LINE of S st
( not A on L & L on P )

proof end;

theorem Th50: :: INCSP_1:50

for S being IncSpace
for A being POINT of S
for P being PLANE of S st A on P holds
ex L, L1, L2 being LINE of S st
( L1 <> L2 & L1 on P & L2 on P & not L on P & A on L & A on L1 & A on L2 )

proof end;

theorem :: INCSP_1:51

for S being IncSpace
for A being POINT of S ex L, L1, L2 being LINE of S st
( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ) )

proof end;

theorem :: INCSP_1:52

for S being IncSpace
for A being POINT of S
for L being LINE of S ex P being PLANE of S st
( A on P & not L on P )

proof end;

theorem :: INCSP_1:53

for S being IncSpace
for L being LINE of S
for P being PLANE of S ex A being POINT of S st
( A on P & not A on L )

proof end;

theorem :: INCSP_1:54

for S being IncSpace
for L being LINE of S ex K being LINE of S st
for P being PLANE of S holds
( not L on P or not K on P )

proof end;

theorem :: INCSP_1:55

for S being IncSpace
for L being LINE of S ex P, Q being PLANE of S st
( P <> Q & L on P & L on Q )

proof end;

:: Intersection of lines and planes

theorem :: INCSP_1:56

for S being IncSpace
for A, B being POINT of S
for L being LINE of S
for P being PLANE of S st not L on P & {A,B} on L & {A,B} on P holds
A = B by Def14;

theorem :: INCSP_1:57

for S being 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 ) )

proof end;