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:11;
A2: LeftComp (SpStSeq D) c= UBD (L~ (SpStSeq D)) by Th99;
A3: RightComp (SpStSeq D) c= BDD (L~ (SpStSeq D)) by Th102;

A4: now

assume not LeftComp (SpStSeq D) = UBD (L~ (SpStSeq D)) ; :: thesis: contradiction
then not UBD (L~ (SpStSeq D)) c= LeftComp (SpStSeq D) by A2, XBOOLE_0:def 10;
then consider z being set such that
A5: z in UBD (L~ (SpStSeq D)) and
A6: not z in LeftComp (SpStSeq D) by TARSKI:def 3;
UBD (L~ (SpStSeq D)) c= (L~ (SpStSeq D)) ` by Th30;
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 Th28; :: thesis: verum

end;

now

assume not RightComp (SpStSeq D) = BDD (L~ (SpStSeq D)) ; :: thesis: contradiction
then not BDD (L~ (SpStSeq D)) c= RightComp (SpStSeq D) by A3, XBOOLE_0:def 10;
then consider z being set such that
A7: z in BDD (L~ (SpStSeq D)) and
A8: not z in RightComp (SpStSeq D) by TARSKI:def 3;
BDD (L~ (SpStSeq D)) c= (L~ (SpStSeq D)) ` by Th29;
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 Th28; :: thesis: verum

end;

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