assume A8: S ` <> {} ; :: thesis: ( for A1, A2 being Subset of (TOP-REAL 2) holds
( not S ` = A1 \/ A2 or not A1 misses A2 or not (Cl A1) \ A1 = (Cl A2) \ A2 or not A1 is_a_component_of S ` or not A2 is_a_component_of S ` ) or S is Jordan )
given A1, A2 being Subset of (TOP-REAL 2) such that A9: S ` = A1 \/ A2 and
A10: A1 misses A2 and
A11: (Cl A1) \ A1 = (Cl A2) \ A2 and
A12: A1 is_a_component_of S ` and
A13: A2 is_a_component_of S ` ; :: thesis: S is Jordan
reconsider a1 = A1, a2 = A2 as Subset of (TOP-REAL 2) ;
A14: ex B being Subset of ((TOP-REAL 2) | (S `)) st
( B = a2 & B is a_component ) by A13, CONNSP_1:def 6;
thus S ` <> {} by A8; :: according to JORDAN1:def 2 :: thesis: ex b<sub>1</sub>, b<sub>2</sub> being Element of bool the carrier of (TOP-REAL 2) st
( S ` = b₁ \/ b₂ & b₁ misses b₂ & (Cl b₁) \ b₁ = (Cl b₂) \ b₂ & ( for b₃, b₄ being Element of bool the carrier of ((TOP-REAL 2) | (S `)) holds
( not b<sub>3</sub> = b<sub>1</sub> or not b<sub>4</sub> = b<sub>2</sub> or ( b<sub>3</sub> is a_component & b<sub>4</sub> is a_component ) ) ) )
take a1 ; :: thesis: ex b<sub>1</sub> being Element of bool the carrier of (TOP-REAL 2) st
( S ` = a1 \/ b₁ & a1 misses b₁ & (Cl a1) \ a1 = (Cl b₁) \ b₁ & ( for b₂, b₃ being Element of bool the carrier of ((TOP-REAL 2) | (S `)) holds
( not b<sub>2</sub> = a1 or not b<sub>3</sub> = b<sub>1</sub> or ( b<sub>2</sub> is a_component & b<sub>3</sub> is a_component ) ) ) )
take a2 ; :: thesis: ( S ` = a1 \/ a2 & a1 misses a2 & (Cl a1) \ a1 = (Cl a2) \ a2 & ( for b₁, b₂ being Element of bool the carrier of ((TOP-REAL 2) | (S `)) holds
( not b<sub>1</sub> = a1 or not b<sub>2</sub> = a2 or ( b<sub>1</sub> is a_component & b<sub>2</sub> is a_component ) ) ) )
thus S ` = a1 \/ a2 by A9; :: thesis: ( a1 misses a2 & (Cl a1) \ a1 = (Cl a2) \ a2 & ( for b₁, b₂ being Element of bool the carrier of ((TOP-REAL 2) | (S `)) holds
( not b<sub>1</sub> = a1 or not b<sub>2</sub> = a2 or ( b<sub>1</sub> is a_component & b<sub>2</sub> is a_component ) ) ) )
thus a1 /\ a2 = {} by A10; :: according to XBOOLE_0:def 7 :: thesis: ( (Cl a1) \ a1 = (Cl a2) \ a2 & ( for b<sub>1</sub>, b<sub>2</sub> being Element of bool the carrier of ((TOP-REAL 2) | (S `)) holds
( not b₁ = a1 or not b₂ = a2 or ( b₁ is a_component & b₂ is a_component ) ) ) )
thus (Cl a1) \ a1 = (Cl a2) \ a2 by A11; :: thesis: for b₁, b₂ being Element of bool the carrier of ((TOP-REAL 2) | (S `)) holds
( not b<sub>1</sub> = a1 or not b<sub>2</sub> = a2 or ( b<sub>1</sub> is a_component & b<sub>2</sub> is a_component ) )
ex B being Subset of ((TOP-REAL 2) | (S `)) st
( B = a1 & B is a_component ) by A12, CONNSP_1:def 6;
hence for b₁, b₂ being Element of bool the carrier of ((TOP-REAL 2) | (S `)) holds
( not b₁ = a1 or not b₂ = a2 or ( b₁ is a_component & b₂ is a_component ) ) by A14; :: thesis: verum