environ
vocabularies HIDDEN, NUMBERS, REAL_1, NAT_1, XBOOLE_0, SUBSET_1, PRE_TOPC, EUCLID, FUNCT_1, BORSUK_1, RELAT_1, TOPS_2, CARD_1, STRUCT_0, XXREAL_1, RLTOPSP1, TARSKI, ARYTM_1, ARYTM_3, XXREAL_0, MCART_1, SUPINF_2, RCOMP_1, PCOMPS_1, CONNSP_2, TOPMETR, METRIC_1, TOPS_1, COMPLEX1, ORDINAL2, FINSEQ_1, PARTFUN1, ZFMISC_1, SETFAM_1, TOPREAL1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, TOPS_1, TOPS_2, CONNSP_2, COMPTS_1, RCOMP_1, FINSEQ_1, FINSEQ_4, STRUCT_0, METRIC_1, TOPMETR, PCOMPS_1, RLVECT_1, RLTOPSP1, EUCLID, PRE_TOPC, XXREAL_0;
definitions TARSKI, XBOOLE_0, FUNCT_1, PRE_TOPC;
theorems BORSUK_1, COMPTS_1, CONNSP_2, ENUMSET1, EUCLID, FINSEQ_1, FUNCT_1, FUNCT_2, HEINE, METRIC_1, NAT_1, PCOMPS_1, PRE_TOPC, RCOMP_1, TARSKI, TOPMETR, TOPMETR2, TOPS_1, TOPS_2, ZFMISC_1, FINSEQ_3, FINSEQ_4, TBSP_1, PARTFUN2, RELSET_1, RELAT_1, INT_1, XBOOLE_0, XBOOLE_1, XREAL_0, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, XXREAL_1, RLTOPSP1, RLVECT_1;
schemes NAT_1, CLASSES1, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, PCOMPS_1, BORSUK_1, EUCLID, TOPMETR, VALUED_0, RLTOPSP1, FUNCT_1, ORDINAL1;
constructors HIDDEN, SETFAM_1, REAL_1, NAT_1, COMPLEX1, FINSEQOP, RCOMP_1, FINSEQ_4, TOPS_1, TOPS_2, COMPTS_1, EUCLID, TOPMETR, RVSUM_1, VALUED_1, FUNCSDOM, RLTOPSP1, CONVEX1, BINOP_2, PCOMPS_1, RUSUB_4;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities EUCLID, STRUCT_0, RLTOPSP1, RLVECT_1;
expansions TARSKI, XBOOLE_0, FUNCT_1, PRE_TOPC;
definition
func R^2-unit_square -> Subset of
(TOP-REAL 2) equals
((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|)));
coherence
((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|))) is Subset of (TOP-REAL 2)
;
end;
::
deftheorem defines
R^2-unit_square TOPREAL1:def 2 :
R^2-unit_square = ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[0,0]|)));
Lm1:
for n being Nat
for p, p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) holds
LSeg (p1,p) c= LSeg (p1,p2)
Lm2:
for T being TopSpace holds
( T is T_2 iff TopStruct(# the carrier of T, the topology of T #) is T_2 )
theorem Th13:
(
LSeg (
|[0,0]|,
|[0,1]|)
= { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = 0 & p1 `2 <= 1 & p1 `2 >= 0 ) } &
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 ) } )