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