let AS be AffinSpace; :: thesis: for x being set holds
( x is POINT of (IncProjSp_of AS) iff ( x is Element of AS or ex X being Subset of AS st
( x = LDir X & X is being_line ) ) )
let x be set ; :: thesis: ( x is POINT of (IncProjSp_of AS) iff ( x is Element of AS or ex X being Subset of AS st
( x = LDir X & X is being_line ) ) )

A1: now

assume A2: x is POINT of (IncProjSp_of AS) ; :: thesis: ( x is Element of AS or ex X being Subset of AS st
( x = LDir X & X is being_line ) )
( x in Dir_of_Lines AS implies ex X being Subset of AS st
( x = LDir X & X is being_line ) ) by Th14;
hence ( x is Element of AS or ex X being Subset of AS st
( x = LDir X & X is being_line ) ) by A2, XBOOLE_0:def 3; :: thesis: verum

end;

now

assume A3: ( x is Element of AS or ex X being Subset of AS st
( x = LDir X & X is being_line ) ) ; :: thesis: x is POINT of (IncProjSp_of AS)

now

given X being Subset of AS such that A4: ( x = LDir X & X is being_line ) ; :: thesis: x is POINT of (IncProjSp_of AS)
x in Dir_of_Lines AS by A4, Th14;
hence x is POINT of (IncProjSp_of AS) by XBOOLE_0:def 3; :: thesis: verum

end;

hence x is POINT of (IncProjSp_of AS) by A3, XBOOLE_0:def 3; :: thesis: verum

end;

hence ( x is POINT of (IncProjSp_of AS) iff ( x is Element of AS or ex X being Subset of AS st
( x = LDir X & X is being_line ) ) ) by A1; :: thesis: verum