let AS be AffinSpace; :: thesis: 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 ; :: thesis: ( 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 ) ) )

A1: now

assume A2: x is LINE of (IncProjSp_of AS) ; :: thesis: ex X being Subset of AS st
( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) )
A3: ( 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;
( 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;
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 A2, A3, XBOOLE_0:def 3; :: thesis: verum

end;

now

given X being Subset of AS such that A4: ( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) ; :: thesis: x is LINE of (IncProjSp_of AS)

A5: now

assume ( x = [X,1] & X is being_line ) ; :: thesis: x is LINE of (IncProjSp_of AS)
then x in [:(AfLines AS),{1}:] by Th18;
hence x is LINE of (IncProjSp_of AS) by XBOOLE_0:def 3; :: thesis: verum

end;

now

assume ( x = [(PDir X),2] & X is being_plane ) ; :: thesis: x is LINE of (IncProjSp_of AS)
then x in [:(Dir_of_Planes AS),{2}:] by Th19;
hence x is LINE of (IncProjSp_of AS) by XBOOLE_0:def 3; :: thesis: verum

end;

hence x is LINE of (IncProjSp_of AS) by A4, A5; :: thesis: 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; :: thesis: verum