let AS be AffinSpace; for x being set holds
( x is LINE of (IncProjSp_of AS) iff ex X being Subset of AS st
( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) )
let x be set ; ( x is LINE of (IncProjSp_of AS) iff ex X being Subset of AS st
( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) )
now ( x is LINE of (IncProjSp_of AS) implies ex X being Subset of AS st
( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) )A8:
(
x in [:(Dir_of_Planes AS),{2}:] implies ex
X being
Subset of
AS st
( (
x = [X,1] &
X is
being_line ) or (
x = [(PDir X),2] &
X is
being_plane ) ) )
by Th19;
assume A9:
x is
LINE of
(IncProjSp_of AS)
;
ex X being Subset of AS st
( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) )
(
x in [:(AfLines AS),{1}:] implies ex
X being
Subset of
AS st
( (
x = [X,1] &
X is
being_line ) or (
x = [(PDir X),2] &
X is
being_plane ) ) )
by Th18;
hence
ex
X being
Subset of
AS st
( (
x = [X,1] &
X is
being_line ) or (
x = [(PDir X),2] &
X is
being_plane ) )
by A9, A8, XBOOLE_0:def 3;
verum end;
hence
( x is LINE of (IncProjSp_of AS) iff ex X being Subset of AS st
( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) )
by A1; verum