let AS be AffinSpace; :: thesis: for a, b being Element of the Points of (ProjHorizon AS) ex A being Element of the Lines of (ProjHorizon AS) st
( a on A & b on A )
let a, b be Element of the Points of (ProjHorizon AS); :: thesis: ex A being Element of the Lines of (ProjHorizon AS) st
( a on A & b on A )
consider X being Subset of AS such that
A1: ( a = LDir X & X is being_line ) by Th14;
consider X' being Subset of AS such that
A2: ( b = LDir X' & X' is being_line ) by Th14;
consider x, y being Element of AS such that
A3: x in X' and
( y in X' & x <> y ) by A2, AFF_1:31;
A4: ( x * X is being_line & x in x * X & X // x * X ) by A1, AFF_4:27, AFF_4:def 3;
then consider Z being Subset of AS such that
A5: ( X' c= Z & x * X c= Z & Z is being_plane ) by A2, A3, AFF_4:38;
reconsider A = PDir Z as Element of the Lines of (ProjHorizon AS) by A5, Th15;
take A ; :: thesis: ( a on A & b on A )
( X '||' Z & X' '||' Z ) by A1, A2, A4, A5, AFF_4:41, AFF_4:42;
hence ( a on A & b on A ) by A1, A2, A5, Th36; :: thesis: verum