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 :: thesis: ( ex X being Subset of AS st
( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) implies x is LINE of (IncProjSp_of AS) )
given X being Subset of AS such that A2: ( ( x = [X,1] & X is being_line ) or ( x = [(PDir X),2] & X is being_plane ) ) ; :: thesis: x is LINE of (IncProjSp_of AS)
A3: now :: thesis: ( x = [(PDir X),2] & X is being_plane implies x is LINE of (IncProjSp_of AS) )
assume that
A4: x = [(PDir X),2] and
A5: X is being_plane ; :: thesis: x is LINE of (IncProjSp_of AS)
x in [:(Dir_of_Planes AS),{2}:] by A4, A5, Th19;
hence x is LINE of (IncProjSp_of AS) by XBOOLE_0:def 3; :: thesis: verum
end;
now :: thesis: ( x = [X,1] & X is being_line implies x is LINE of (IncProjSp_of AS) )
assume that
A6: x = [X,1] and
A7: X is being_line ; :: thesis: x is LINE of (IncProjSp_of AS)
x in [:(AfLines AS),{1}:] by A6, A7, Th18;
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 A2, A3; :: thesis: verum
end;
now :: thesis: ( 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) ; :: thesis: 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; :: 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