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 ) } ;
set p0 = |[0 ,0 ]|;
set p01 = |[0 ,1]|;
set p10 = |[1,0 ]|;
set p1 = |[1,1]|;
A1:
( |[0 ,1]| `1 = 0 & |[0 ,1]| `2 = 1 )
by EUCLID:56;
A2:
( |[1,1]| `1 = 1 & |[1,1]| `2 = 1 )
by EUCLID:56;
A3:
( |[1,0 ]| `1 = 1 & |[1,0 ]| `2 = 0 )
by EUCLID:56;
thus
{ p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) } = LSeg |[0 ,0 ]|,|[0 ,1]|
:: thesis: ( 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 ) } )proof
A4:
{ 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
set ;
:: according to TARSKI:def 3 :: thesis: ( 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 ) }
;
:: thesis: a in LSeg |[0 ,0 ]|,|[0 ,1]|
then consider p being
Point of
(TOP-REAL 2) such that A5:
a = p
and A6:
(
p `1 = 0 &
p `2 <= 1 &
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 Lm1, EUCLID:32
.=
(p `2 ) * |[0 ,1]|
by EUCLID:31
.=
|[((p `2 ) * (|[0 ,1]| `1 )),((p `2 ) * (|[0 ,1]| `2 ))]|
by EUCLID:61
.=
p
by A1, A6, EUCLID:57
;
hence
a in LSeg |[0 ,0 ]|,
|[0 ,1]|
by A5, A6;
:: thesis: verum
end;
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
set ;
:: according to TARSKI:def 3 :: thesis: ( 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]|
;
:: thesis: 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 A7:
(
a = ((1 - lambda) * |[0 ,0 ]|) + (lambda * |[0 ,1]|) &
0 <= lambda &
lambda <= 1 )
;
set q =
((1 - lambda) * |[0 ,0 ]|) + (lambda * |[0 ,1]|);
((1 - lambda) * |[0 ,0 ]|) + (lambda * |[0 ,1]|) =
(0. (TOP-REAL 2)) + (lambda * |[0 ,1]|)
by Lm1, EUCLID:32
.=
lambda * |[0 ,1]|
by EUCLID:31
.=
|[(lambda * (|[0 ,1]| `1 )),(lambda * (|[0 ,1]| `2 ))]|
by EUCLID:61
.=
|[0 ,lambda]|
by A1
;
then
(
(((1 - lambda) * |[0 ,0 ]|) + (lambda * |[0 ,1]|)) `1 = 0 &
(((1 - lambda) * |[0 ,0 ]|) + (lambda * |[0 ,1]|)) `2 <= 1 &
(((1 - lambda) * |[0 ,0 ]|) + (lambda * |[0 ,1]|)) `2 >= 0 )
by A7, EUCLID:56;
hence
a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 0 & p `2 <= 1 & p `2 >= 0 ) }
by A7;
:: thesis: 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 A4, XBOOLE_0:def 10;
:: thesis: verum
end;
thus
{ p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) } = LSeg |[0 ,1]|,|[1,1]|
:: thesis: ( 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 ) } )proof
A8:
{ 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
set ;
:: according to TARSKI:def 3 :: thesis: ( 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 ) }
;
:: thesis: a in LSeg |[0 ,1]|,|[1,1]|
then consider p being
Point of
(TOP-REAL 2) such that A9:
a = p
and A10:
(
p `1 <= 1 &
p `1 >= 0 &
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 A1, EUCLID:61
.=
|[0 ,(1 - (p `1 ))]| + |[((p `1 ) * 1),(p `1 )]|
by A1, A2, EUCLID:61
.=
|[(0 + (p `1 )),((1 - (p `1 )) + (p `1 ))]|
by EUCLID:60
.=
p
by A10, EUCLID:57
;
hence
a in LSeg |[0 ,1]|,
|[1,1]|
by A9, A10;
:: thesis: verum
end;
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
set ;
:: according to TARSKI:def 3 :: thesis: ( 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]|
;
:: thesis: 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 A11:
(
a = ((1 - lambda) * |[0 ,1]|) + (lambda * |[1,1]|) &
0 <= lambda &
lambda <= 1 )
;
set q =
((1 - lambda) * |[0 ,1]|) + (lambda * |[1,1]|);
((1 - lambda) * |[0 ,1]|) + (lambda * |[1,1]|) =
|[((1 - lambda) * 0 ),((1 - lambda) * (|[0 ,1]| `2 ))]| + (lambda * |[1,1]|)
by A1, EUCLID:61
.=
|[0 ,(1 - lambda)]| + |[lambda,(lambda * 1)]|
by A1, A2, EUCLID:61
.=
|[(0 + lambda),((1 - lambda) + lambda)]|
by EUCLID:60
.=
|[lambda,1]|
;
then
(
(((1 - lambda) * |[0 ,1]|) + (lambda * |[1,1]|)) `1 <= 1 &
(((1 - lambda) * |[0 ,1]|) + (lambda * |[1,1]|)) `1 >= 0 &
(((1 - lambda) * |[0 ,1]|) + (lambda * |[1,1]|)) `2 = 1 )
by A11, EUCLID:56;
hence
a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 1 ) }
by A11;
:: thesis: 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 A8, XBOOLE_0:def 10;
:: thesis: verum
end;
thus
{ p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) } = LSeg |[0 ,0 ]|,|[1,0 ]|
:: thesis: LSeg |[1,0 ]|,|[1,1]| = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = 1 & q2 `2 <= 1 & q2 `2 >= 0 ) } proof
A12:
{ 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
set ;
:: according to TARSKI:def 3 :: thesis: ( 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 ) }
;
:: thesis: a in LSeg |[0 ,0 ]|,|[1,0 ]|
then consider p being
Point of
(TOP-REAL 2) such that A13:
a = p
and A14:
(
p `1 <= 1 &
p `1 >= 0 &
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 Lm1, EUCLID:32
.=
(p `1 ) * |[1,0 ]|
by EUCLID:31
.=
|[((p `1 ) * (|[1,0 ]| `1 )),((p `1 ) * (|[1,0 ]| `2 ))]|
by EUCLID:61
.=
p
by A3, A14, EUCLID:57
;
hence
a in LSeg |[0 ,0 ]|,
|[1,0 ]|
by A13, A14;
:: thesis: verum
end;
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
set ;
:: according to TARSKI:def 3 :: thesis: ( 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 ]|
;
:: thesis: 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 A15:
(
a = ((1 - lambda) * |[0 ,0 ]|) + (lambda * |[1,0 ]|) &
0 <= lambda &
lambda <= 1 )
;
set q =
((1 - lambda) * |[0 ,0 ]|) + (lambda * |[1,0 ]|);
((1 - lambda) * |[0 ,0 ]|) + (lambda * |[1,0 ]|) =
(0. (TOP-REAL 2)) + (lambda * |[1,0 ]|)
by Lm1, EUCLID:32
.=
lambda * |[1,0 ]|
by EUCLID:31
.=
|[(lambda * (|[1,0 ]| `1 )),(lambda * (|[1,0 ]| `2 ))]|
by EUCLID:61
.=
|[lambda,0 ]|
by A3
;
then
(
(((1 - lambda) * |[0 ,0 ]|) + (lambda * |[1,0 ]|)) `1 <= 1 &
(((1 - lambda) * |[0 ,0 ]|) + (lambda * |[1,0 ]|)) `1 >= 0 &
(((1 - lambda) * |[0 ,0 ]|) + (lambda * |[1,0 ]|)) `2 = 0 )
by A15, EUCLID:56;
hence
a in { p where p is Point of (TOP-REAL 2) : ( p `1 <= 1 & p `1 >= 0 & p `2 = 0 ) }
by A15;
:: thesis: 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 A12, XBOOLE_0:def 10;
:: thesis: verum
end;
thus
{ p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) } = LSeg |[1,0 ]|,|[1,1]|
:: thesis: verumproof
A16:
{ 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
set ;
:: according to TARSKI:def 3 :: thesis: ( 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 ) }
;
:: thesis: a in LSeg |[1,0 ]|,|[1,1]|
then consider p being
Point of
(TOP-REAL 2) such that A17:
a = p
and A18:
(
p `1 = 1 &
p `2 <= 1 &
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 A3, EUCLID:61
.=
|[(1 - (p `2 )),0 ]| + |[((p `2 ) * 1),(p `2 )]|
by A2, A3, EUCLID:61
.=
|[((1 - (p `2 )) + (p `2 )),(0 + (p `2 ))]|
by EUCLID:60
.=
p
by A18, EUCLID:57
;
hence
a in LSeg |[1,0 ]|,
|[1,1]|
by A17, A18;
:: thesis: verum
end;
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
set ;
:: according to TARSKI:def 3 :: thesis: ( 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]|
;
:: thesis: 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 A19:
(
a = ((1 - lambda) * |[1,0 ]|) + (lambda * |[1,1]|) &
0 <= lambda &
lambda <= 1 )
;
set q =
((1 - lambda) * |[1,0 ]|) + (lambda * |[1,1]|);
((1 - lambda) * |[1,0 ]|) + (lambda * |[1,1]|) =
|[((1 - lambda) * 1),((1 - lambda) * (|[1,0 ]| `2 ))]| + (lambda * |[1,1]|)
by A3, EUCLID:61
.=
|[(1 - lambda),0 ]| + |[lambda,(lambda * 1)]|
by A2, A3, EUCLID:61
.=
|[((1 - lambda) + lambda),(0 + lambda)]|
by EUCLID:60
.=
|[1,lambda]|
;
then
(
(((1 - lambda) * |[1,0 ]|) + (lambda * |[1,1]|)) `1 = 1 &
(((1 - lambda) * |[1,0 ]|) + (lambda * |[1,1]|)) `2 <= 1 &
(((1 - lambda) * |[1,0 ]|) + (lambda * |[1,1]|)) `2 >= 0 )
by A19, EUCLID:56;
hence
a in { p where p is Point of (TOP-REAL 2) : ( p `1 = 1 & p `2 <= 1 & p `2 >= 0 ) }
by A19;
:: thesis: 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 A16, XBOOLE_0:def 10;
:: thesis: verum
end;