let A, B be Subset of (TOP-REAL 2); for s being Real st A misses B & A c= Horizontal_Line s & B c= Horizontal_Line s holds
proj1 .: A misses proj1 .: B
let s be Real; ( A misses B & A c= Horizontal_Line s & B c= Horizontal_Line s implies proj1 .: A misses proj1 .: B )
assume that
A1:
A misses B
and
A2:
A c= Horizontal_Line s
and
A3:
B c= Horizontal_Line s
; proj1 .: A misses proj1 .: B
assume
proj1 .: A meets proj1 .: B
; contradiction
then consider e being object such that
A4:
e in proj1 .: A
and
A5:
e in proj1 .: B
by XBOOLE_0:3;
reconsider e = e as Real by A4;
consider d being Point of (TOP-REAL 2) such that
A6:
d in B
and
A7:
e = proj1 . d
by A5, FUNCT_2:65;
A8:
d `2 = s
by A3, A6, JORDAN6:32;
consider c being Point of (TOP-REAL 2) such that
A9:
c in A
and
A10:
e = proj1 . c
by A4, FUNCT_2:65;
c `2 = s
by A2, A9, JORDAN6:32;
then c =
|[(c `1),(d `2)]|
by A8, EUCLID:53
.=
|[e,(d `2)]|
by A10, PSCOMP_1:def 5
.=
|[(d `1),(d `2)]|
by A7, PSCOMP_1:def 5
.=
d
by EUCLID:53
;
hence
contradiction
by A1, A9, A6, XBOOLE_0:3; verum