let AS be AffinSpace; :: thesis: for A being Element of the Lines of (ProjHorizon AS) ex a, b, c being Element of the Points of (ProjHorizon AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
let A be Element of the Lines of (ProjHorizon AS); :: thesis: ex a, b, c being Element of the Points of (ProjHorizon AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
consider X being Subset of AS such that
A1:
A = PDir X
and
A2:
X is being_plane
by Th15;
consider x, y, z being Element of AS such that
A3:
( x in X & y in X & z in X )
and
A4:
not LIN x,y,z
by A2, AFF_4:34;
A5:
( x <> y & y <> z & z <> x )
by A4, AFF_1:16;
then A6:
( Line x,y is being_line & Line y,z is being_line & Line x,z is being_line )
by AFF_1:def 3;
then reconsider a = LDir (Line x,y), b = LDir (Line y,z), c = LDir (Line x,z) as Element of the Points of (ProjHorizon AS) by Th14;
take
a
; :: thesis: ex b, c being Element of the Points of (ProjHorizon AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
take
b
; :: thesis: ex c being Element of the Points of (ProjHorizon AS) st
( a on A & b on A & c on A & a <> b & b <> c & c <> a )
take
c
; :: thesis: ( a on A & b on A & c on A & a <> b & b <> c & c <> a )
( Line x,y '||' X & Line y,z '||' X & Line x,z '||' X )
by A2, A3, A5, A6, AFF_4:19, AFF_4:42;
hence
( a on A & b on A & c on A )
by A1, A2, A6, Th36; :: thesis: ( a <> b & b <> c & c <> a )
A7:
( x in Line x,y & y in Line x,y & y in Line y,z & z in Line y,z & x in Line x,z & z in Line x,z )
by AFF_1:26;
thus
a <> b
:: thesis: ( b <> c & c <> a )
thus
b <> c
:: thesis: c <> a
thus
c <> a
:: thesis: verum