let C be Simple_closed_curve; :: thesis: for i being Element of NAT holds Fr ((UBD (L~ (Cage C,i))) ` ) = L~ (Cage C,i)
let i be Element of 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:18;
UBD (L~ (Cage C,i)) c= (L~ (Cage C,i)) ` by JORDAN2C:30;
then A2: UBD (L~ (Cage C,i)) misses L~ (Cage C,i) by SUBSET_1:43;
UBD (L~ (Cage C,i)) misses BDD (L~ (Cage C,i)) by JORDAN2C:28;
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:18
.= ((BDD (L~ (Cage C,i))) \/ (UBD (L~ (Cage C,i)))) \/ (L~ (Cage C,i)) by JORDAN2C:31 ;
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:31;
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:52;
A6: ((UBD (L~ (Cage C,i))) ` ) ` = LeftComp (Cage C,i) by GOBRD14:46;
BDD (L~ (Cage C,i)) misses UBD (L~ (Cage C,i)) by JORDAN2C:28;
then A7: (BDD (L~ (Cage C,i))) /\ (UBD (L~ (Cage C,i))) = {} by XBOOLE_0:def 7;
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:32
.= ((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