let A, B be Subset of (TOP-REAL 2); :: thesis: ( A meets B implies proj2 .: A meets proj2 .: B )
assume A meets B ; :: thesis: proj2 .: A meets proj2 .: B
then consider e being object such that
A1: e in A and
A2: e in B by XBOOLE_0:3;
reconsider e = e as Point of (TOP-REAL 2) by A1;
e `2 = proj2 . e by PSCOMP_1:def 6;
then ( e `2 in proj2 .: A & e `2 in proj2 .: B ) by A1, A2, FUNCT_2:35;
hence proj2 .: A meets proj2 .: B by XBOOLE_0:3; :: thesis: verum