defpred S1[ Point of (TOP-REAL 2)] means ( $1 `1 = 1 & $1 `2 <= 1 & $1 `2 >= 0 );
defpred S2[ Point of (TOP-REAL 2)] means ( $1 `1 <= 1 & $1 `1 >= 0 & $1 `2 = 0 );
defpred S3[ Point of (TOP-REAL 2)] means ( $1 `1 <= 1 & $1 `1 >= 0 & $1 `2 = 1 );
defpred S4[ Point of (TOP-REAL 2)] means ( $1 `1 = 0 & $1 `2 <= 1 & $1 `2 >= 0 );
defpred S5[ Point of (TOP-REAL 2)] means ( ( $1 `1 <= 1 & $1 `1 >= 0 & $1 `2 = 0 ) or ( $1 `1 = 1 & $1 `2 <= 1 & $1 `2 >= 0 ) );
defpred S6[ Point of (TOP-REAL 2)] means ( ( $1 `1 = 0 & $1 `2 <= 1 & $1 `2 >= 0 ) or ( $1 `1 <= 1 & $1 `1 >= 0 & $1 `2 = 1 ) );
set L1 = { p where p is Point of (TOP-REAL 2) : S4[p] } ;
set L2 = { p where p is Point of (TOP-REAL 2) : S3[p] } ;
set L3 = { p where p is Point of (TOP-REAL 2) : S2[p] } ;
set L4 = { p where p is Point of (TOP-REAL 2) : S1[p] } ;
A1:
{ p2 where p2 is Point of (TOP-REAL 2) : ( S6[p2] or S5[p2] ) } = { p where p is Point of (TOP-REAL 2) : S6[p] } \/ { q1 where q1 is Point of (TOP-REAL 2) : S5[q1] }
from TOPREAL1:sch 1();
A2: { q1 where q1 is Point of (TOP-REAL 2) : ( S2[q1] or S1[q1] ) } =
{ p where p is Point of (TOP-REAL 2) : S2[p] } \/ { p where p is Point of (TOP-REAL 2) : S1[p] }
from TOPREAL1:sch 1()
.=
(LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))
by Th13
;
{ p where p is Point of (TOP-REAL 2) : ( S4[p] or S3[p] ) } =
{ p where p is Point of (TOP-REAL 2) : S4[p] } \/ { p where p is Point of (TOP-REAL 2) : S3[p] }
from TOPREAL1:sch 1()
.=
(LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))
by Th13
;
hence
R^2-unit_square = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) or ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) or ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) or ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) ) }
by A1, A2; verum