let D be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( LeftComp (SpStSeq D) = UBD (L~ (SpStSeq D)) & RightComp (SpStSeq D) = BDD (L~ (SpStSeq D)) )
set f = SpStSeq D;
A1: (L~ (SpStSeq D)) ` = (LeftComp (SpStSeq D)) \/ (RightComp (SpStSeq D)) by GOBRD12:10;
A2: LeftComp (SpStSeq D) c= UBD (L~ (SpStSeq D)) by Th75;
A3: RightComp (SpStSeq D) c= BDD (L~ (SpStSeq D)) by Th78;

A4: now :: thesis: LeftComp (SpStSeq D) = UBD (L~ (SpStSeq D))

assume not LeftComp (SpStSeq D) = UBD (L~ (SpStSeq D)) ; :: thesis: contradiction
then not UBD (L~ (SpStSeq D)) c= LeftComp (SpStSeq D) by A2;
then consider z being object such that
A5: z in UBD (L~ (SpStSeq D)) and
A6: not z in LeftComp (SpStSeq D) ;
UBD (L~ (SpStSeq D)) c= (L~ (SpStSeq D)) ` by Th17;
then ( z in LeftComp (SpStSeq D) or z in RightComp (SpStSeq D) ) by A1, A5, XBOOLE_0:def 3;
then BDD (L~ (SpStSeq D)) meets UBD (L~ (SpStSeq D)) by A3, A5, A6, XBOOLE_0:3;
hence contradiction by Th15; :: thesis: verum

end;

now :: thesis: RightComp (SpStSeq D) = BDD (L~ (SpStSeq D))

assume not RightComp (SpStSeq D) = BDD (L~ (SpStSeq D)) ; :: thesis: contradiction
then not BDD (L~ (SpStSeq D)) c= RightComp (SpStSeq D) by A3;
then consider z being object such that
A7: z in BDD (L~ (SpStSeq D)) and
A8: not z in RightComp (SpStSeq D) ;
BDD (L~ (SpStSeq D)) c= (L~ (SpStSeq D)) ` by Th16;
then ( z in LeftComp (SpStSeq D) or z in RightComp (SpStSeq D) ) by A1, A7, XBOOLE_0:def 3;
then BDD (L~ (SpStSeq D)) meets UBD (L~ (SpStSeq D)) by A2, A7, A8, XBOOLE_0:3;
hence contradiction by Th15; :: thesis: verum

end;

hence ( LeftComp (SpStSeq D) = UBD (L~ (SpStSeq D)) & RightComp (SpStSeq D) = BDD (L~ (SpStSeq D)) ) by A4; :: thesis: verum