thus (L~ f) ` <> {} ; :: according to SPRECT_1:def 3 :: thesis: ex b<sub>1</sub>, b<sub>2</sub> being Element of K19( the carrier of (TOP-REAL 2)) st
( (L~ f) ` = b₁ \/ b₂ & b₁ misses b₂ & (Cl b₁) \ b₁ = (Cl b₂) \ b₂ & b₁ is_a_component_of (L~ f) ` & b<sub>2</sub> is_a_component_of (L~ f) ` )
take A1 = RightComp f; :: thesis: ex b₁ being Element of K19( the carrier of (TOP-REAL 2)) st
( (L~ f) ` = A1 \/ b<sub>1</sub> & A1 misses b<sub>1</sub> & (Cl A1) \ A1 = (Cl b<sub>1</sub>) \ b<sub>1</sub> & A1 is_a_component_of (L~ f) ` & b₁ is_a_component_of (L~ f) ` )
take A2 = LeftComp f; :: thesis: ( (L~ f) ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A1 is_a_component_of (L~ f) ` & A2 is_a_component_of (L~ f) ` )
thus (L~ f) ` = A1 \/ A2 by GOBRD12:10; :: thesis: ( A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A1 is_a_component_of (L~ f) ` & A2 is_a_component_of (L~ f) ` )
L~ f = (Cl A1) \ A1 by Th19;
hence ( A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A1 is_a_component_of (L~ f) ` & A2 is_a_component_of (L~ f) ` ) by Th14, Th20, GOBOARD9:def 1, GOBOARD9:def 2; :: thesis: verum