let X be non empty TopSpace; :: thesis: for X0, X1, X2 being non empty SubSpace of X holds

( ( not X1 union X2 meets X0 or X1 meets X0 or X2 meets X0 ) & ( ( X1 meets X0 or X2 meets X0 ) implies X1 union X2 meets X0 ) & ( not X0 meets X1 union X2 or X0 meets X1 or X0 meets X2 ) & ( ( X0 meets X1 or X0 meets X2 ) implies X0 meets X1 union X2 ) )

let X0, X1, X2 be non empty SubSpace of X; :: thesis: ( ( not X1 union X2 meets X0 or X1 meets X0 or X2 meets X0 ) & ( ( X1 meets X0 or X2 meets X0 ) implies X1 union X2 meets X0 ) & ( not X0 meets X1 union X2 or X0 meets X1 or X0 meets X2 ) & ( ( X0 meets X1 or X0 meets X2 ) implies X0 meets X1 union 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;

A1: ( ( X1 meets X0 or X2 meets X0 ) implies X1 union X2 meets X0 )

thus ( ( X0 meets X1 or X0 meets X2 ) iff X0 meets X1 union X2 ) by A2, A1; :: thesis: verum

( ( not X1 union X2 meets X0 or X1 meets X0 or X2 meets X0 ) & ( ( X1 meets X0 or X2 meets X0 ) implies X1 union X2 meets X0 ) & ( not X0 meets X1 union X2 or X0 meets X1 or X0 meets X2 ) & ( ( X0 meets X1 or X0 meets X2 ) implies X0 meets X1 union X2 ) )

let X0, X1, X2 be non empty SubSpace of X; :: thesis: ( ( not X1 union X2 meets X0 or X1 meets X0 or X2 meets X0 ) & ( ( X1 meets X0 or X2 meets X0 ) implies X1 union X2 meets X0 ) & ( not X0 meets X1 union X2 or X0 meets X1 or X0 meets X2 ) & ( ( X0 meets X1 or X0 meets X2 ) implies X0 meets X1 union 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;

A1: ( ( X1 meets X0 or X2 meets X0 ) implies X1 union X2 meets X0 )

proof

A2:
( not X1 union X2 meets X0 or X1 meets X0 or X2 meets X0 )
assume
( X1 meets X0 or X2 meets X0 )
; :: thesis: X1 union X2 meets X0

then ( A1 meets A0 or A2 meets A0 ) by TSEP_1:def 3;

then (A1 /\ A0) \/ (A2 /\ A0) <> {} ;

then (A1 \/ A2) /\ A0 <> {} by XBOOLE_1:23;

then the carrier of (X1 union X2) meets A0 by TSEP_1:def 2;

hence X1 union X2 meets X0 by TSEP_1:def 3; :: thesis: verum

end;then ( A1 meets A0 or A2 meets A0 ) by TSEP_1:def 3;

then (A1 /\ A0) \/ (A2 /\ A0) <> {} ;

then (A1 \/ A2) /\ A0 <> {} by XBOOLE_1:23;

then the carrier of (X1 union X2) meets A0 by TSEP_1:def 2;

hence X1 union X2 meets X0 by TSEP_1:def 3; :: thesis: verum

proof

hence
( ( X1 meets X0 or X2 meets X0 ) iff X1 union X2 meets X0 )
by A1; :: thesis: ( ( X0 meets X1 or X0 meets X2 ) iff X0 meets X1 union X2 )
assume
X1 union X2 meets X0
; :: thesis: ( X1 meets X0 or X2 meets X0 )

then the carrier of (X1 union X2) meets A0 by TSEP_1:def 3;

then the carrier of (X1 union X2) /\ A0 <> {} ;

then (A1 \/ A2) /\ A0 <> {} by TSEP_1:def 2;

then (A1 /\ A0) \/ (A2 /\ A0) <> {} by XBOOLE_1:23;

then ( A1 meets A0 or A2 meets A0 ) ;

hence ( X1 meets X0 or X2 meets X0 ) by TSEP_1:def 3; :: thesis: verum

end;then the carrier of (X1 union X2) meets A0 by TSEP_1:def 3;

then the carrier of (X1 union X2) /\ A0 <> {} ;

then (A1 \/ A2) /\ A0 <> {} by TSEP_1:def 2;

then (A1 /\ A0) \/ (A2 /\ A0) <> {} by XBOOLE_1:23;

then ( A1 meets A0 or A2 meets A0 ) ;

hence ( X1 meets X0 or X2 meets X0 ) by TSEP_1:def 3; :: thesis: verum

thus ( ( X0 meets X1 or X0 meets X2 ) iff X0 meets X1 union X2 ) by A2, A1; :: thesis: verum