let AS be AffinSpace; :: thesis: for A, K being LINE of (IncProjSp_of AS) st AS is AffinPlane holds
ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K )
let A, K be LINE of (IncProjSp_of AS); :: thesis: ( AS is AffinPlane implies ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K ) )
consider X being Subset of AS such that
A1: ( ( A = [X,1] & X is being_line ) or ( A = [(PDir X),2] & X is being_plane ) ) by Th23;
consider X9 being Subset of AS such that
A2: ( ( K = [X9,1] & X9 is being_line ) or ( K = [(PDir X9),2] & X9 is being_plane ) ) by Th23;
assume A3: AS is AffinPlane ; :: thesis: ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K )
A4: now :: thesis: ( A = [X,1] & X is being_line implies ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K ) )
assume that
A5: A = [X,1] and
A6: X is being_line ; :: thesis: ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K )
A7: now :: thesis: ( K = [X9,1] & X9 is being_line implies ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K ) )
assume that
A8: K = [X9,1] and
A9: X9 is being_line ; :: thesis: ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K )
A10: now :: thesis: ( X // X9 implies ex a being Element of the Points of (IncProjSp_of AS) st
( a on A & a on K ) )
reconsider a = LDir X, b = LDir X9 as Element of the Points of (IncProjSp_of AS) by A6, A9, Th20;
X9 // X9 by A9, AFF_1:41;
then A11: X9 '||' X9 by A9, AFF_4:40;
assume X // X9 ; :: thesis: ex a being Element of the Points of (IncProjSp_of AS) st
( a on A & a on K )
then A12: a = b by A6, A9, Th11;
take a = a; :: thesis: ( a on A & a on K )
X // X by A6, AFF_1:41;
then X '||' X by A6, AFF_4:40;
hence ( a on A & a on K ) by A5, A6, A8, A9, A12, A11, Th28; :: thesis: verum
end;
now :: thesis: ( not X // X9 implies ex a being Element of the Points of (IncProjSp_of AS) st
( a on A & a on K ) )
assume not X // X9 ; :: thesis: ex a being Element of the Points of (IncProjSp_of AS) st
( a on A & a on K )
then consider x being Element of AS such that
A13: x in X and
A14: x in X9 by A3, A6, A9, AFF_1:58;
reconsider a = x as Element of the Points of (IncProjSp_of AS) by Th20;
take a = a; :: thesis: ( a on A & a on K )
thus ( a on A & a on K ) by A5, A6, A8, A9, A13, A14, Th26; :: thesis: verum
end;
hence ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K ) by A10; :: thesis: verum
end;
now :: thesis: ( K = [(PDir X9),2] & X9 is being_plane implies ex a being Element of the Points of (IncProjSp_of AS) st
( a on A & a on K ) )
X // X by A6, AFF_1:41;
then A15: X '||' X by A6, AFF_4:40;
reconsider a = LDir X as Element of the Points of (IncProjSp_of AS) by A6, Th20;
assume that
A16: K = [(PDir X9),2] and
A17: X9 is being_plane ; :: thesis: ex a being Element of the Points of (IncProjSp_of AS) st
( a on A & a on K )
take a = a; :: thesis: ( a on A & a on K )
X9 = the carrier of AS by A3, A17, Th2;
then X '||' X9 by A6, A17, AFF_4:42;
hence ( a on A & a on K ) by A5, A6, A16, A17, A15, Th28, Th29; :: thesis: verum
end;
hence ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K ) by A2, A7; :: thesis: verum
end;
now :: thesis: ( A = [(PDir X),2] & X is being_plane implies ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K ) )
assume that
A18: A = [(PDir X),2] and
A19: X is being_plane ; :: thesis: ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K )
A20: X = the carrier of AS by A3, A19, Th2;
A21: now :: thesis: ( K = [X9,1] & X9 is being_line implies ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K ) )
assume that
A22: K = [X9,1] and
A23: X9 is being_line ; :: thesis: ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K )
X9 // X9 by A23, AFF_1:41;
then A24: X9 '||' X9 by A23, AFF_4:40;
reconsider a = LDir X9 as POINT of (IncProjSp_of AS) by A23, Th20;
take a = a; :: thesis: ( a on A & a on K )
X9 '||' X by A19, A20, A23, AFF_4:42;
hence ( a on A & a on K ) by A18, A19, A22, A23, A24, Th28, Th29; :: thesis: verum
end;
now :: thesis: ( K = [(PDir X9),2] & X9 is being_plane implies ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K ) )
consider a, b, c being POINT of (IncProjSp_of AS) such that
A25: a on A and
b on A and
c on A and
a <> b and
b <> c and
c <> a by Lm3;
assume that
A26: K = [(PDir X9),2] and
A27: X9 is being_plane ; :: thesis: ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K )
take a = a; :: thesis: ( a on A & a on K )
thus ( a on A & a on K ) by A3, A18, A19, A26, A27, A25, Th3; :: thesis: verum
end;
hence ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K ) by A2, A21; :: thesis: verum
end;
hence ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K ) by A1, A4; :: thesis: verum