let A, B be Subset of (TOP-REAL 2); ( A meets B implies proj1 .: A meets proj1 .: B )
assume
A meets B
; proj1 .: A meets proj1 .: 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;
A3:
e `1 = proj1 . e
by PSCOMP_1:def 5;
then A4:
e `1 in proj1 .: B
by A2, FUNCT_2:35;
e `1 in proj1 .: A
by A1, A3, FUNCT_2:35;
hence
proj1 .: A meets proj1 .: B
by A4, XBOOLE_0:3; verum