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