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