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:56;
A2: |[0 ,1]| `1 = 0 by EUCLID:56;
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 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
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:32, EUCLID:58
.= lambda * |[0 ,1]| by EUCLID:31
.= |[(lambda * (|[0 ,1]| `1 )),(lambda * (|[0 ,1]| `2 ))]| by EUCLID:61
.= |[0 ,lambda]| by A2, A1 ;
then A8: (((1 - lambda) * |[0 ,0 ]|) + (lambda * |[0 ,1]|)) `2 >= 0 by A5, EUCLID:56;
A9: (((1 - lambda) * |[0 ,0 ]|) + (lambda * |[0 ,1]|)) `1 = 0 by A7, EUCLID:56;
(((1 - lambda) * |[0 ,0 ]|) + (lambda * |[0 ,1]|)) `2 <= 1 by A6, 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 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 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
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:32, EUCLID:58
.= (p `2 ) * |[0 ,1]| by EUCLID:31
.= |[((p `2 ) * (|[0 ,1]| `1 )),((p `2 ) * (|[0 ,1]| `2 ))]| by EUCLID:61
.= p by A2, A1, A11, EUCLID:57 ;
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, XBOOLE_0:def 10; :: 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:56;
A15: |[1,1]| `1 = 1 by EUCLID:56;
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 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
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:61
.= |[0 ,(1 - lambda)]| + |[lambda,(lambda * 1)]| by A1, A15, A14, EUCLID:61
.= |[(0 + lambda),((1 - lambda) + lambda)]| by EUCLID:60
.= |[lambda,1]| ;
then A21: (((1 - lambda) * |[0 ,1]|) + (lambda * |[1,1]|)) `1 >= 0 by A18, EUCLID:56;
A22: (((1 - lambda) * |[0 ,1]|) + (lambda * |[1,1]|)) `2 = 1 by A20, EUCLID:56;
(((1 - lambda) * |[0 ,1]|) + (lambda * |[1,1]|)) `1 <= 1 by A19, A20, EUCLID:56;
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 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
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:61
.= |[0 ,(1 - (p `1 ))]| + |[((p `1 ) * 1),(p `1 )]| by A1, A15, A14, EUCLID:61
.= |[(0 + (p `1 )),((1 - (p `1 )) + (p `1 ))]| by EUCLID:60
.= p by A26, EUCLID:57 ;
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, XBOOLE_0:def 10; :: 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:56;
A28: |[1,0 ]| `1 = 1 by EUCLID:56;
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 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
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:32, EUCLID:58
.= lambda * |[1,0 ]| by EUCLID:31
.= |[(lambda * (|[1,0 ]| `1 )),(lambda * (|[1,0 ]| `2 ))]| by EUCLID:61
.= |[lambda,0 ]| by A28, A27 ;
then A34: (((1 - lambda) * |[0 ,0 ]|) + (lambda * |[1,0 ]|)) `1 >= 0 by A31, EUCLID:56;
A35: (((1 - lambda) * |[0 ,0 ]|) + (lambda * |[1,0 ]|)) `2 = 0 by A33, EUCLID:56;
(((1 - lambda) * |[0 ,0 ]|) + (lambda * |[1,0 ]|)) `1 <= 1 by A32, A33, EUCLID:56;
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 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
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:61
.= |[(1 - lambda),0 ]| + |[lambda,(lambda * 1)]| by A15, A14, A27, EUCLID:61
.= |[((1 - lambda) + lambda),(0 + lambda)]| by EUCLID:60
.= |[1,lambda]| ;
then A41: (((1 - lambda) * |[1,0 ]|) + (lambda * |[1,1]|)) `2 >= 0 by A38, EUCLID:56;
A42: (((1 - lambda) * |[1,0 ]|) + (lambda * |[1,1]|)) `1 = 1 by A40, EUCLID:56;
(((1 - lambda) * |[1,0 ]|) + (lambda * |[1,1]|)) `2 <= 1 by A39, A40, EUCLID:56;
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 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
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:32, EUCLID:58
.= (p `1 ) * |[1,0 ]| by EUCLID:31
.= |[((p `1 ) * (|[1,0 ]| `1 )),((p `1 ) * (|[1,0 ]| `2 ))]| by EUCLID:61
.= p by A28, A27, A46, EUCLID:57 ;
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, XBOOLE_0:def 10; :: 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 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
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:61
.= |[(1 - (p `2 )),0 ]| + |[((p `2 ) * 1),(p `2 )]| by A15, A14, A27, EUCLID:61
.= |[((1 - (p `2 )) + (p `2 )),(0 + (p `2 ))]| by EUCLID:60
.= p by A48, EUCLID:57 ;
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, XBOOLE_0:def 10; :: thesis: verum