let s be real number ; 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 set 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:116;
A8:
d `1 = s
by A3, A6, JORDAN6:34;
consider c being Point of (TOP-REAL 2) such that
A9:
c in A
and
A10:
e = proj2 . c
by A4, FUNCT_2:116;
c `1 = s
by A2, A9, JORDAN6:34;
then c =
|[(d `1 ),(c `2 )]|
by A8, EUCLID:57
.=
|[(d `1 ),e]|
by A10, PSCOMP_1:def 29
.=
|[(d `1 ),(d `2 )]|
by A7, PSCOMP_1:def 29
.=
d
by EUCLID:57
;
hence
contradiction
by A1, A9, A6, XBOOLE_0:3; verum