environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, REAL_1, XBOOLE_0, PRE_TOPC, SQUARE_1, XXREAL_0, CARD_1, RELAT_2, TARSKI, CONNSP_1, SETFAM_1, RCOMP_1, CONNSP_3, ZFMISC_1, STRUCT_0, FUNCT_1, GOBOARD5, RELAT_1, MATRIX_1, EUCLID, TOPREAL1, RLTOPSP1, ARYTM_3, GOBOARD2, TREES_1, ARYTM_1, FINSEQ_1, MCART_1, GOBOARD1, TOPS_1, PCOMPS_1, METRIC_1, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SEQM_3, TOPREAL1, GOBOARD1, ORDINAL1, XXREAL_0, NUMBERS, BINOP_1, XCMPLX_0, XREAL_0, REAL_1, NAT_1, NAT_D, SQUARE_1, MATRIX_0, STRUCT_0, PRE_TOPC, FINSEQ_1, MATRIX_1, METRIC_1, TOPS_1, CONNSP_1, PCOMPS_1, RLVECT_1, RLTOPSP1, EUCLID, GOBOARD2, GOBOARD5, CONNSP_3;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, NAT_1, SPPOL_1, GOBOARD7, GOBOARD8, PRE_TOPC, CONNSP_1, SUBSET_1, EUCLID, CONNSP_3, GOBOARD5, TOPS_1, TOPMETR, SPPOL_2, SQUARE_1, METRIC_1, GOBOARD6, TOPREAL3, JORDAN1, ZFMISC_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, MATRIX_0;
schemes NAT_1;
registrations SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, STRUCT_0, PRE_TOPC, EUCLID, GOBOARD1, GOBOARD2, GOBOARD5, RLTOPSP1, SQUARE_1, ORDINAL1, NAT_1;
constructors HIDDEN, SETFAM_1, REAL_1, SQUARE_1, TOPS_1, CONNSP_1, PCOMPS_1, GOBOARD2, GOBOARD5, CONNSP_3, GOBOARD1, NAT_D, FUNCSDOM, CONVEX1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, EUCLID, SQUARE_1;
expansions TARSKI, XBOOLE_0;
Lm1:
sqrt 2 > 0
by SQUARE_1:25;
Lm2:
the carrier of (TOP-REAL 2) = REAL 2
by EUCLID:22;
Lm3:
for s1 being Real holds { |[tb,sb]| where tb, sb is Real : sb >= s1 } is Subset of (TOP-REAL 2)
Lm4:
for s1 being Real holds { |[tb,sb]| where tb, sb is Real : sb > s1 } is Subset of (TOP-REAL 2)
Lm5:
for s1 being Real holds { |[tb,sb]| where tb, sb is Real : sb <= s1 } is Subset of (TOP-REAL 2)
Lm6:
for s1 being Real holds { |[tb,sb]| where tb, sb is Real : sb < s1 } is Subset of (TOP-REAL 2)
Lm7:
for s1 being Real holds { |[sb,tb]| where sb, tb is Real : sb <= s1 } is Subset of (TOP-REAL 2)
Lm8:
for s1 being Real holds { |[sb,tb]| where sb, tb is Real : sb < s1 } is Subset of (TOP-REAL 2)
Lm9:
for s1 being Real holds { |[sb,tb]| where sb, tb is Real : sb >= s1 } is Subset of (TOP-REAL 2)
Lm10:
for s1 being Real holds { |[sb,tb]| where sb, tb is Real : sb > s1 } is Subset of (TOP-REAL 2)