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

A1: now

A2: now

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

end;

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

end;

now

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

end;

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