let C be Simple_closed_curve; :: thesis: for i being Nat holds Fr ((UBD (L~ (Cage (C,i)))) `) = L~ (Cage (C,i))
let i be Nat; :: thesis: Fr ((UBD (L~ (Cage (C,i)))) `) = L~ (Cage (C,i))
set K = (UBD (L~ (Cage (C,i)))) ` ;
set R = L~ (Cage (C,i));
A1: (BDD (L~ (Cage (C,i)))) \/ ((BDD (L~ (Cage (C,i)))) `) = [#] (TOP-REAL 2) by PRE_TOPC:2;
UBD (L~ (Cage (C,i))) c= (L~ (Cage (C,i))) ` by JORDAN2C:26;
then A2: UBD (L~ (Cage (C,i))) misses L~ (Cage (C,i)) by SUBSET_1:23;
UBD (L~ (Cage (C,i))) misses BDD (L~ (Cage (C,i))) by JORDAN2C:24;
then A3: UBD (L~ (Cage (C,i))) misses (BDD (L~ (Cage (C,i)))) \/ (L~ (Cage (C,i))) by A2, XBOOLE_1:70;
[#] (TOP-REAL 2) = ((L~ (Cage (C,i))) `) \/ (L~ (Cage (C,i))) by PRE_TOPC:2
.= ((BDD (L~ (Cage (C,i)))) \/ (UBD (L~ (Cage (C,i))))) \/ (L~ (Cage (C,i))) by JORDAN2C:27 ;
then A4: (UBD (L~ (Cage (C,i)))) ` = ((UBD (L~ (Cage (C,i)))) \/ ((BDD (L~ (Cage (C,i)))) \/ (L~ (Cage (C,i))))) \ (UBD (L~ (Cage (C,i)))) by XBOOLE_1:4
.= (L~ (Cage (C,i))) \/ (BDD (L~ (Cage (C,i)))) by A3, XBOOLE_1:88 ;
((BDD (L~ (Cage (C,i)))) \/ (UBD (L~ (Cage (C,i))))) ` = ((L~ (Cage (C,i))) `) ` by JORDAN2C:27;
then ((BDD (L~ (Cage (C,i)))) `) /\ ((UBD (L~ (Cage (C,i)))) `) = L~ (Cage (C,i)) by XBOOLE_1:53;
then (BDD (L~ (Cage (C,i)))) \/ (L~ (Cage (C,i))) = ((BDD (L~ (Cage (C,i)))) \/ ((BDD (L~ (Cage (C,i)))) `)) /\ ((BDD (L~ (Cage (C,i)))) \/ ((UBD (L~ (Cage (C,i)))) `)) by XBOOLE_1:24
.= (BDD (L~ (Cage (C,i)))) \/ ((UBD (L~ (Cage (C,i)))) `) by A1, XBOOLE_1:28
.= (UBD (L~ (Cage (C,i)))) ` by A4, XBOOLE_1:7, XBOOLE_1:12 ;
then A5: Cl ((UBD (L~ (Cage (C,i)))) `) = (BDD (L~ (Cage (C,i)))) \/ (L~ (Cage (C,i))) by PRE_TOPC:22;
A6: ((UBD (L~ (Cage (C,i)))) `) ` = LeftComp (Cage (C,i)) by GOBRD14:36;
BDD (L~ (Cage (C,i))) misses UBD (L~ (Cage (C,i))) by JORDAN2C:24;
then A7: (BDD (L~ (Cage (C,i)))) /\ (UBD (L~ (Cage (C,i)))) = {} ;
Fr ((UBD (L~ (Cage (C,i)))) `) = (Cl ((UBD (L~ (Cage (C,i)))) `)) /\ (Cl (((UBD (L~ (Cage (C,i)))) `) `)) by TOPS_1:def 2
.= ((BDD (L~ (Cage (C,i)))) \/ (L~ (Cage (C,i)))) /\ ((UBD (L~ (Cage (C,i)))) \/ (L~ (Cage (C,i)))) by A5, A6, GOBRD14:22
.= ((BDD (L~ (Cage (C,i)))) /\ (UBD (L~ (Cage (C,i))))) \/ (L~ (Cage (C,i))) by XBOOLE_1:24
.= L~ (Cage (C,i)) by A7 ;
hence Fr ((UBD (L~ (Cage (C,i)))) `) = L~ (Cage (C,i)) ; :: thesis: verum