let X be non empty TopSpace; :: thesis: for X0, X1, X2 being non empty SubSpace of X st X1 meets X2 holds
( ( X1 meet X2 meets X0 implies ( X1 meets X0 & X2 meets X0 ) ) & ( X0 meets X1 meet X2 implies ( X0 meets X1 & X0 meets X2 ) ) )
let X0, X1, X2 be non empty SubSpace of X; :: thesis: ( X1 meets X2 implies ( ( X1 meet X2 meets X0 implies ( X1 meets X0 & X2 meets X0 ) ) & ( X0 meets X1 meet X2 implies ( X0 meets X1 & X0 meets X2 ) ) ) )
reconsider A0 = the carrier of X0 as Subset of X by TSEP_1:1;
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
assume A1: X1 meets X2 ; :: thesis: ( ( X1 meet X2 meets X0 implies ( X1 meets X0 & X2 meets X0 ) ) & ( X0 meets X1 meet X2 implies ( X0 meets X1 & X0 meets X2 ) ) )
thus ( X1 meet X2 meets X0 implies ( X1 meets X0 & X2 meets X0 ) ) :: thesis: ( X0 meets X1 meet X2 implies ( X0 meets X1 & X0 meets X2 ) )
proof
assume X1 meet X2 meets X0 ; :: thesis: ( X1 meets X0 & X2 meets X0 )
then the carrier of (X1 meet X2) meets A0 by TSEP_1:def 3;
then (A1 /\ A2) /\ A0 <> {} by A1, TSEP_1:def 4;
then A2: A1 /\ (A2 /\ (A0 /\ A0)) <> {} by XBOOLE_1:16;
then A1 /\ (A0 /\ (A2 /\ A0)) <> {} by XBOOLE_1:16;
then (A1 /\ A0) /\ (A2 /\ A0) <> {} by XBOOLE_1:16;
then A3: A1 meets A0 ;
A2 /\ A0 <> {} by A2;
then A2 meets A0 ;
hence ( X1 meets X0 & X2 meets X0 ) by A3, TSEP_1:def 3; :: thesis: verum
end;
hence ( X0 meets X1 meet X2 implies ( X0 meets X1 & X0 meets X2 ) ) ; :: thesis: verum