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 :: thesis: ( ( x is Element of AS or ex X being Subset of AS st
( x = LDir X & X is being_line ) ) implies x is POINT of (IncProjSp_of AS) )
A2: now :: thesis: ( ex X being Subset of AS st
( x = LDir X & X is being_line ) implies x is POINT of (IncProjSp_of AS) )
given X being Subset of AS such that A3: x = LDir X and
A4: X is being_line ; :: thesis: x is POINT of (IncProjSp_of AS)
x in Dir_of_Lines AS by A3, A4, Th14;
hence x is POINT of (IncProjSp_of AS) by XBOOLE_0:def 3; :: thesis: verum
end;
assume ( 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)
hence x is POINT of (IncProjSp_of AS) by A2, XBOOLE_0:def 3; :: thesis: verum
end;
now :: thesis: ( not x is POINT of (IncProjSp_of AS) or x is Element of AS or ex X being Subset of AS st
( x = LDir X & X is being_line ) )
assume A5: 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 A5, 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