set p0 = |[0,0]|;
set p01 = |[0,1]|;
set p10 = |[1,0]|;
set p1 = |[1,1]|;
set L1 = { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } ;
set L2 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } ;
set L3 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } ;
set L4 = { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } ;
A1:
|[0,1]| `2 = 1
by EUCLID:52;
A2:
|[0,1]| `1 = 0
by EUCLID:52;
A3:
LSeg (|[0,0]|,|[0,1]|) c= { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) }
proof
let a be
object ;
TARSKI:def 3 ( not a in LSeg (|[0,0]|,|[0,1]|) or a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } )
assume
a in LSeg (
|[0,0]|,
|[0,1]|)
;
a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) }
then consider lambda being
Real such that A4:
a = ((1 - lambda) * |[0,0]|) + (lambda * |[0,1]|)
and A5:
0 <= lambda
and A6:
lambda <= 1
;
set q =
((1 - lambda) * |[0,0]|) + (lambda * |[0,1]|);
A7:
((1 - lambda) * |[0,0]|) + (lambda * |[0,1]|) =
(0. (TOP-REAL 2)) + (lambda * |[0,1]|)
by EUCLID:54, RLVECT_1:10
.=
lambda * |[0,1]|
by RLVECT_1:4
.=
|[(lambda * (|[0,1]| `1)),(lambda * (|[0,1]| `2))]|
by EUCLID:57
.=
|[0,lambda]|
by A2, A1
;
then A8:
(((1 - lambda) * |[0,0]|) + (lambda * |[0,1]|)) `2 >= 0
by A5, EUCLID:52;
A9:
(((1 - lambda) * |[0,0]|) + (lambda * |[0,1]|)) `1 = 0
by A7, EUCLID:52;
(((1 - lambda) * |[0,0]|) + (lambda * |[0,1]|)) `2 <= 1
by A6, A7, EUCLID:52;
hence
a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) }
by A4, A9, A8;
verum
end;
{ p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } c= LSeg (|[0,0]|,|[0,1]|)
proof
let a be
object ;
TARSKI:def 3 ( not a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } or a in LSeg (|[0,0]|,|[0,1]|) )
assume
a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) }
;
a in LSeg (|[0,0]|,|[0,1]|)
then consider p being
Point of
(TOP-REAL 2) such that A10:
a = p
and A11:
p `1 = 0
and A12:
p `2 <= 1
and A13:
p `2 >= 0
;
set lambda =
p `2 ;
((1 - (p `2)) * |[0,0]|) + ((p `2) * |[0,1]|) =
(0. (TOP-REAL 2)) + ((p `2) * |[0,1]|)
by EUCLID:54, RLVECT_1:10
.=
(p `2) * |[0,1]|
by RLVECT_1:4
.=
|[((p `2) * (|[0,1]| `1)),((p `2) * (|[0,1]| `2))]|
by EUCLID:57
.=
p
by A2, A1, A11, EUCLID:53
;
hence
a in LSeg (
|[0,0]|,
|[0,1]|)
by A10, A12, A13;
verum
end;
hence
{ p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } = LSeg (|[0,0]|,|[0,1]|)
by A3; ( LSeg (|[0,1]|,|[1,1]|) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= 1 & p2 `1 >= 0 & p2 `2 = 1 ) } & LSeg (|[0,0]|,|[1,0]|) = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 <= 1 & q1 `1 >= 0 & q1 `2 = 0 ) } & LSeg (|[1,0]|,|[1,1]|) = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = 1 & q2 `2 <= 1 & q2 `2 >= 0 ) } )
A14:
|[1,1]| `2 = 1
by EUCLID:52;
A15:
|[1,1]| `1 = 1
by EUCLID:52;
A16:
LSeg (|[0,1]|,|[1,1]|) c= { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) }
proof
let a be
object ;
TARSKI:def 3 ( not a in LSeg (|[0,1]|,|[1,1]|) or a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } )
assume
a in LSeg (
|[0,1]|,
|[1,1]|)
;
a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) }
then consider lambda being
Real such that A17:
a = ((1 - lambda) * |[0,1]|) + (lambda * |[1,1]|)
and A18:
0 <= lambda
and A19:
lambda <= 1
;
set q =
((1 - lambda) * |[0,1]|) + (lambda * |[1,1]|);
A20:
((1 - lambda) * |[0,1]|) + (lambda * |[1,1]|) =
|[((1 - lambda) * 0),((1 - lambda) * (|[0,1]| `2))]| + (lambda * |[1,1]|)
by A2, EUCLID:57
.=
|[0,(1 - lambda)]| + |[lambda,(lambda * 1)]|
by A1, A15, A14, EUCLID:57
.=
|[(0 + lambda),((1 - lambda) + lambda)]|
by EUCLID:56
.=
|[lambda,1]|
;
then A21:
(((1 - lambda) * |[0,1]|) + (lambda * |[1,1]|)) `1 >= 0
by A18, EUCLID:52;
A22:
(((1 - lambda) * |[0,1]|) + (lambda * |[1,1]|)) `2 = 1
by A20, EUCLID:52;
(((1 - lambda) * |[0,1]|) + (lambda * |[1,1]|)) `1 <= 1
by A19, A20, EUCLID:52;
hence
a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) }
by A17, A21, A22;
verum
end;
{ p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } c= LSeg (|[0,1]|,|[1,1]|)
proof
let a be
object ;
TARSKI:def 3 ( not a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } or a in LSeg (|[0,1]|,|[1,1]|) )
assume
a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) }
;
a in LSeg (|[0,1]|,|[1,1]|)
then consider p being
Point of
(TOP-REAL 2) such that A23:
a = p
and A24:
p `1 <= 1
and A25:
p `1 >= 0
and A26:
p `2 = 1
;
set lambda =
p `1 ;
((1 - (p `1)) * |[0,1]|) + ((p `1) * |[1,1]|) =
|[((1 - (p `1)) * 0),((1 - (p `1)) * (|[0,1]| `2))]| + ((p `1) * |[1,1]|)
by A2, EUCLID:57
.=
|[0,(1 - (p `1))]| + |[((p `1) * 1),(p `1)]|
by A1, A15, A14, EUCLID:57
.=
|[(0 + (p `1)),((1 - (p `1)) + (p `1))]|
by EUCLID:56
.=
p
by A26, EUCLID:53
;
hence
a in LSeg (
|[0,1]|,
|[1,1]|)
by A23, A24, A25;
verum
end;
hence
{ p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } = LSeg (|[0,1]|,|[1,1]|)
by A16; ( LSeg (|[0,0]|,|[1,0]|) = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 <= 1 & q1 `1 >= 0 & q1 `2 = 0 ) } & LSeg (|[1,0]|,|[1,1]|) = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = 1 & q2 `2 <= 1 & q2 `2 >= 0 ) } )
A27:
|[1,0]| `2 = 0
by EUCLID:52;
A28:
|[1,0]| `1 = 1
by EUCLID:52;
A29:
LSeg (|[0,0]|,|[1,0]|) c= { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) }
proof
let a be
object ;
TARSKI:def 3 ( not a in LSeg (|[0,0]|,|[1,0]|) or a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } )
assume
a in LSeg (
|[0,0]|,
|[1,0]|)
;
a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) }
then consider lambda being
Real such that A30:
a = ((1 - lambda) * |[0,0]|) + (lambda * |[1,0]|)
and A31:
0 <= lambda
and A32:
lambda <= 1
;
set q =
((1 - lambda) * |[0,0]|) + (lambda * |[1,0]|);
A33:
((1 - lambda) * |[0,0]|) + (lambda * |[1,0]|) =
(0. (TOP-REAL 2)) + (lambda * |[1,0]|)
by EUCLID:54, RLVECT_1:10
.=
lambda * |[1,0]|
by RLVECT_1:4
.=
|[(lambda * (|[1,0]| `1)),(lambda * (|[1,0]| `2))]|
by EUCLID:57
.=
|[lambda,0]|
by A28, A27
;
then A34:
(((1 - lambda) * |[0,0]|) + (lambda * |[1,0]|)) `1 >= 0
by A31, EUCLID:52;
A35:
(((1 - lambda) * |[0,0]|) + (lambda * |[1,0]|)) `2 = 0
by A33, EUCLID:52;
(((1 - lambda) * |[0,0]|) + (lambda * |[1,0]|)) `1 <= 1
by A32, A33, EUCLID:52;
hence
a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) }
by A30, A34, A35;
verum
end;
A36:
LSeg (|[1,0]|,|[1,1]|) c= { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) }
proof
let a be
object ;
TARSKI:def 3 ( not a in LSeg (|[1,0]|,|[1,1]|) or a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } )
assume
a in LSeg (
|[1,0]|,
|[1,1]|)
;
a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) }
then consider lambda being
Real such that A37:
a = ((1 - lambda) * |[1,0]|) + (lambda * |[1,1]|)
and A38:
0 <= lambda
and A39:
lambda <= 1
;
set q =
((1 - lambda) * |[1,0]|) + (lambda * |[1,1]|);
A40:
((1 - lambda) * |[1,0]|) + (lambda * |[1,1]|) =
|[((1 - lambda) * 1),((1 - lambda) * (|[1,0]| `2))]| + (lambda * |[1,1]|)
by A28, EUCLID:57
.=
|[(1 - lambda),0]| + |[lambda,(lambda * 1)]|
by A15, A14, A27, EUCLID:57
.=
|[((1 - lambda) + lambda),(0 + lambda)]|
by EUCLID:56
.=
|[1,lambda]|
;
then A41:
(((1 - lambda) * |[1,0]|) + (lambda * |[1,1]|)) `2 >= 0
by A38, EUCLID:52;
A42:
(((1 - lambda) * |[1,0]|) + (lambda * |[1,1]|)) `1 = 1
by A40, EUCLID:52;
(((1 - lambda) * |[1,0]|) + (lambda * |[1,1]|)) `2 <= 1
by A39, A40, EUCLID:52;
hence
a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) }
by A37, A42, A41;
verum
end;
{ p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } c= LSeg (|[0,0]|,|[1,0]|)
proof
let a be
object ;
TARSKI:def 3 ( not a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } or a in LSeg (|[0,0]|,|[1,0]|) )
assume
a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) }
;
a in LSeg (|[0,0]|,|[1,0]|)
then consider p being
Point of
(TOP-REAL 2) such that A43:
a = p
and A44:
p `1 <= 1
and A45:
p `1 >= 0
and A46:
p `2 = 0
;
set lambda =
p `1 ;
((1 - (p `1)) * |[0,0]|) + ((p `1) * |[1,0]|) =
(0. (TOP-REAL 2)) + ((p `1) * |[1,0]|)
by EUCLID:54, RLVECT_1:10
.=
(p `1) * |[1,0]|
by RLVECT_1:4
.=
|[((p `1) * (|[1,0]| `1)),((p `1) * (|[1,0]| `2))]|
by EUCLID:57
.=
p
by A28, A27, A46, EUCLID:53
;
hence
a in LSeg (
|[0,0]|,
|[1,0]|)
by A43, A44, A45;
verum
end;
hence
{ p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } = LSeg (|[0,0]|,|[1,0]|)
by A29; LSeg (|[1,0]|,|[1,1]|) = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = 1 & q2 `2 <= 1 & q2 `2 >= 0 ) }
{ p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } c= LSeg (|[1,0]|,|[1,1]|)
proof
let a be
object ;
TARSKI:def 3 ( not a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } or a in LSeg (|[1,0]|,|[1,1]|) )
assume
a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) }
;
a in LSeg (|[1,0]|,|[1,1]|)
then consider p being
Point of
(TOP-REAL 2) such that A47:
a = p
and A48:
p `1 = 1
and A49:
p `2 <= 1
and A50:
p `2 >= 0
;
set lambda =
p `2 ;
((1 - (p `2)) * |[1,0]|) + ((p `2) * |[1,1]|) =
|[((1 - (p `2)) * 1),((1 - (p `2)) * (|[1,0]| `2))]| + ((p `2) * |[1,1]|)
by A28, EUCLID:57
.=
|[(1 - (p `2)),0]| + |[((p `2) * 1),(p `2)]|
by A15, A14, A27, EUCLID:57
.=
|[((1 - (p `2)) + (p `2)),(0 + (p `2))]|
by EUCLID:56
.=
p
by A48, EUCLID:53
;
hence
a in LSeg (
|[1,0]|,
|[1,1]|)
by A47, A49, A50;
verum
end;
hence
{ p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } = LSeg (|[1,0]|,|[1,1]|)
by A36; verum