let A, B be Subset of (TOP-REAL 2); :: thesis: ( A meets B implies proj1 .: A meets proj1 .: B )

assume A meets B ; :: thesis: 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; :: thesis: verum

assume A meets B ; :: thesis: 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; :: thesis: verum