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 ; :: 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
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; :: thesis: 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 ; :: 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
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; :: 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 A3; :: 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 ) } )
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 ; :: 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
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; :: thesis: 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 ; :: 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
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; :: 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 A16; :: 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 ) } )
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 ; :: 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
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; :: thesis: 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 ; :: 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
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; :: thesis: 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 ; :: 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
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; :: 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 A29; :: thesis: 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 ; :: 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
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; :: 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 A36; :: thesis: verum