:: YELLOW12 semantic presentation begin registration let X be empty set ; cluster union X -> empty ; coherence union X is empty by ZFMISC_1:2; end; Lm1: now__::_thesis:_for_S,_T,_x1,_x2_being_set_st_x1_in_S_&_x2_in_T_holds_ <:(pr2_(S,T)),(pr1_(S,T)):>_._(x1,x2)_=_[x2,x1] let S, T, x1, x2 be set ; ::_thesis: ( x1 in S & x2 in T implies <:(pr2 (S,T)),(pr1 (S,T)):> . (x1,x2) = [x2,x1] ) assume A1: ( x1 in S & x2 in T ) ; ::_thesis: <:(pr2 (S,T)),(pr1 (S,T)):> . (x1,x2) = [x2,x1] A2: dom <:(pr2 (S,T)),(pr1 (S,T)):> = (dom (pr2 (S,T))) /\ (dom (pr1 (S,T))) by FUNCT_3:def_7 .= (dom (pr2 (S,T))) /\ [:S,T:] by FUNCT_3:def_4 .= [:S,T:] /\ [:S,T:] by FUNCT_3:def_5 .= [:S,T:] ; [x1,x2] in [:S,T:] by A1, ZFMISC_1:87; hence <:(pr2 (S,T)),(pr1 (S,T)):> . (x1,x2) = [((pr2 (S,T)) . (x1,x2)),((pr1 (S,T)) . (x1,x2))] by A2, FUNCT_3:def_7 .= [x2,((pr1 (S,T)) . (x1,x2))] by A1, FUNCT_3:def_5 .= [x2,x1] by A1, FUNCT_3:def_4 ; ::_thesis: verum end; theorem :: YELLOW12:1 for X, A being set holds (delta X) .: A c= [:A,A:] proof let X, A be set ; ::_thesis: (delta X) .: A c= [:A,A:] set f = delta X; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (delta X) .: A or y in [:A,A:] ) assume y in (delta X) .: A ; ::_thesis: y in [:A,A:] then consider x being set such that A1: x in dom (delta X) and A2: x in A and A3: y = (delta X) . x by FUNCT_1:def_6; y = [x,x] by A1, A3, FUNCT_3:def_6; hence y in [:A,A:] by A2, ZFMISC_1:def_2; ::_thesis: verum end; theorem Th2: :: YELLOW12:2 for X, A being set holds (delta X) " [:A,A:] c= A proof let X, A be set ; ::_thesis: (delta X) " [:A,A:] c= A set f = delta X; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (delta X) " [:A,A:] or x in A ) assume x in (delta X) " [:A,A:] ; ::_thesis: x in A then ( (delta X) . x in [:A,A:] & (delta X) . x = [x,x] ) by FUNCT_1:def_7, FUNCT_3:def_6; hence x in A by ZFMISC_1:87; ::_thesis: verum end; theorem :: YELLOW12:3 for X being set for A being Subset of X holds (delta X) " [:A,A:] = A proof let X be set ; ::_thesis: for A being Subset of X holds (delta X) " [:A,A:] = A let A be Subset of X; ::_thesis: (delta X) " [:A,A:] = A set f = delta X; thus (delta X) " [:A,A:] c= A by Th2; :: according to XBOOLE_0:def_10 ::_thesis: A c= (delta X) " [:A,A:] let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in (delta X) " [:A,A:] ) assume A1: x in A ; ::_thesis: x in (delta X) " [:A,A:] then (delta X) . x = [x,x] by FUNCT_3:def_6; then ( dom (delta X) = X & (delta X) . x in [:A,A:] ) by A1, FUNCT_3:def_6, ZFMISC_1:87; hence x in (delta X) " [:A,A:] by A1, FUNCT_1:def_7; ::_thesis: verum end; theorem Th4: :: YELLOW12:4 for X, Y being set holds ( dom <:(pr2 (X,Y)),(pr1 (X,Y)):> = [:X,Y:] & rng <:(pr2 (X,Y)),(pr1 (X,Y)):> = [:Y,X:] ) proof let X, Y be set ; ::_thesis: ( dom <:(pr2 (X,Y)),(pr1 (X,Y)):> = [:X,Y:] & rng <:(pr2 (X,Y)),(pr1 (X,Y)):> = [:Y,X:] ) set f = <:(pr2 (X,Y)),(pr1 (X,Y)):>; thus A1: dom <:(pr2 (X,Y)),(pr1 (X,Y)):> = (dom (pr2 (X,Y))) /\ (dom (pr1 (X,Y))) by FUNCT_3:def_7 .= (dom (pr2 (X,Y))) /\ [:X,Y:] by FUNCT_3:def_4 .= [:X,Y:] /\ [:X,Y:] by FUNCT_3:def_5 .= [:X,Y:] ; ::_thesis: rng <:(pr2 (X,Y)),(pr1 (X,Y)):> = [:Y,X:] rng <:(pr2 (X,Y)),(pr1 (X,Y)):> c= [:(rng (pr2 (X,Y))),(rng (pr1 (X,Y))):] by FUNCT_3:51; hence rng <:(pr2 (X,Y)),(pr1 (X,Y)):> c= [:Y,X:] by XBOOLE_1:1; :: according to XBOOLE_0:def_10 ::_thesis: [:Y,X:] c= rng <:(pr2 (X,Y)),(pr1 (X,Y)):> let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in [:Y,X:] or y in rng <:(pr2 (X,Y)),(pr1 (X,Y)):> ) assume y in [:Y,X:] ; ::_thesis: y in rng <:(pr2 (X,Y)),(pr1 (X,Y)):> then consider y1, y2 being set such that A2: ( y1 in Y & y2 in X ) and A3: y = [y1,y2] by ZFMISC_1:def_2; A4: [y2,y1] in dom <:(pr2 (X,Y)),(pr1 (X,Y)):> by A1, A2, ZFMISC_1:87; <:(pr2 (X,Y)),(pr1 (X,Y)):> . (y2,y1) = y by A2, A3, Lm1; hence y in rng <:(pr2 (X,Y)),(pr1 (X,Y)):> by A4, FUNCT_1:def_3; ::_thesis: verum end; theorem Th5: :: YELLOW12:5 for X, Y, A, B being set holds <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] c= [:B,A:] proof let X, Y, A, B be set ; ::_thesis: <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] c= [:B,A:] set f = <:(pr2 (X,Y)),(pr1 (X,Y)):>; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] or y in [:B,A:] ) assume y in <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] ; ::_thesis: y in [:B,A:] then consider x being set such that A1: x in dom <:(pr2 (X,Y)),(pr1 (X,Y)):> and A2: x in [:A,B:] and A3: y = <:(pr2 (X,Y)),(pr1 (X,Y)):> . x by FUNCT_1:def_6; consider x1, x2 being set such that A4: ( x1 in A & x2 in B ) and A5: x = [x1,x2] by A2, ZFMISC_1:def_2; dom <:(pr2 (X,Y)),(pr1 (X,Y)):> = [:X,Y:] by Th4; then ( x1 in X & x2 in Y ) by A1, A5, ZFMISC_1:87; then <:(pr2 (X,Y)),(pr1 (X,Y)):> . (x1,x2) = [x2,x1] by Lm1; hence y in [:B,A:] by A3, A4, A5, ZFMISC_1:87; ::_thesis: verum end; theorem :: YELLOW12:6 for X, Y being set for A being Subset of X for B being Subset of Y holds <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] = [:B,A:] proof let X, Y be set ; ::_thesis: for A being Subset of X for B being Subset of Y holds <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] = [:B,A:] let A be Subset of X; ::_thesis: for B being Subset of Y holds <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] = [:B,A:] let B be Subset of Y; ::_thesis: <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] = [:B,A:] set f = <:(pr2 (X,Y)),(pr1 (X,Y)):>; A1: dom <:(pr2 (X,Y)),(pr1 (X,Y)):> = [:X,Y:] by Th4; thus <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] c= [:B,A:] by Th5; :: according to XBOOLE_0:def_10 ::_thesis: [:B,A:] c= <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in [:B,A:] or y in <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] ) assume y in [:B,A:] ; ::_thesis: y in <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] then consider y1, y2 being set such that A2: ( y1 in B & y2 in A ) and A3: y = [y1,y2] by ZFMISC_1:def_2; ( [y2,y1] in [:A,B:] & <:(pr2 (X,Y)),(pr1 (X,Y)):> . (y2,y1) = [y1,y2] ) by A2, Lm1, ZFMISC_1:87; hence y in <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] by A1, A3, FUNCT_1:def_6; ::_thesis: verum end; theorem Th7: :: YELLOW12:7 for X, Y being set holds <:(pr2 (X,Y)),(pr1 (X,Y)):> is one-to-one proof let X, Y be set ; ::_thesis: <:(pr2 (X,Y)),(pr1 (X,Y)):> is one-to-one set f = <:(pr2 (X,Y)),(pr1 (X,Y)):>; let x, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x in dom <:(pr2 (X,Y)),(pr1 (X,Y)):> or not y in dom <:(pr2 (X,Y)),(pr1 (X,Y)):> or not <:(pr2 (X,Y)),(pr1 (X,Y)):> . x = <:(pr2 (X,Y)),(pr1 (X,Y)):> . y or x = y ) assume that A1: x in dom <:(pr2 (X,Y)),(pr1 (X,Y)):> and A2: y in dom <:(pr2 (X,Y)),(pr1 (X,Y)):> and A3: <:(pr2 (X,Y)),(pr1 (X,Y)):> . x = <:(pr2 (X,Y)),(pr1 (X,Y)):> . y ; ::_thesis: x = y A4: dom <:(pr2 (X,Y)),(pr1 (X,Y)):> = [:X,Y:] by Th4; then consider x1, x2 being set such that A5: ( x1 in X & x2 in Y ) and A6: x = [x1,x2] by A1, ZFMISC_1:def_2; consider y1, y2 being set such that A7: ( y1 in X & y2 in Y ) and A8: y = [y1,y2] by A4, A2, ZFMISC_1:def_2; A9: <:(pr2 (X,Y)),(pr1 (X,Y)):> . (y1,y2) = [y2,y1] by A7, Lm1; A10: <:(pr2 (X,Y)),(pr1 (X,Y)):> . (x1,x2) = [x2,x1] by A5, Lm1; then x1 = y1 by A3, A6, A8, A9, XTUPLE_0:1; hence x = y by A3, A6, A8, A10, A9, XTUPLE_0:1; ::_thesis: verum end; registration let X, Y be set ; cluster<:(pr2 (X,Y)),(pr1 (X,Y)):> -> one-to-one ; coherence <:(pr2 (X,Y)),(pr1 (X,Y)):> is one-to-one by Th7; end; theorem Th8: :: YELLOW12:8 for X, Y being set holds <:(pr2 (X,Y)),(pr1 (X,Y)):> " = <:(pr2 (Y,X)),(pr1 (Y,X)):> proof let X, Y be set ; ::_thesis: <:(pr2 (X,Y)),(pr1 (X,Y)):> " = <:(pr2 (Y,X)),(pr1 (Y,X)):> set f = <:(pr2 (X,Y)),(pr1 (X,Y)):>; set g = <:(pr2 (Y,X)),(pr1 (Y,X)):>; A1: dom (<:(pr2 (X,Y)),(pr1 (X,Y)):> ") = rng <:(pr2 (X,Y)),(pr1 (X,Y)):> by FUNCT_1:32 .= [:Y,X:] by Th4 ; A2: now__::_thesis:_for_x_being_set_st_x_in_[:Y,X:]_holds_ (<:(pr2_(X,Y)),(pr1_(X,Y)):>_")_._x_=_<:(pr2_(Y,X)),(pr1_(Y,X)):>_._x let x be set ; ::_thesis: ( x in [:Y,X:] implies (<:(pr2 (X,Y)),(pr1 (X,Y)):> ") . x = <:(pr2 (Y,X)),(pr1 (Y,X)):> . x ) assume x in [:Y,X:] ; ::_thesis: (<:(pr2 (X,Y)),(pr1 (X,Y)):> ") . x = <:(pr2 (Y,X)),(pr1 (Y,X)):> . x then consider x1, x2 being set such that A3: ( x1 in Y & x2 in X ) and A4: x = [x1,x2] by ZFMISC_1:def_2; A5: ( <:(pr2 (Y,X)),(pr1 (Y,X)):> . (x1,x2) = [x2,x1] & <:(pr2 (X,Y)),(pr1 (X,Y)):> . (x2,x1) = [x1,x2] ) by A3, Lm1; dom <:(pr2 (X,Y)),(pr1 (X,Y)):> = [:X,Y:] by Th4; then [x2,x1] in dom <:(pr2 (X,Y)),(pr1 (X,Y)):> by A3, ZFMISC_1:87; hence (<:(pr2 (X,Y)),(pr1 (X,Y)):> ") . x = <:(pr2 (Y,X)),(pr1 (Y,X)):> . x by A4, A5, FUNCT_1:32; ::_thesis: verum end; dom <:(pr2 (Y,X)),(pr1 (Y,X)):> = [:Y,X:] by Th4; hence <:(pr2 (X,Y)),(pr1 (X,Y)):> " = <:(pr2 (Y,X)),(pr1 (Y,X)):> by A1, A2, FUNCT_1:2; ::_thesis: verum end; begin theorem Th9: :: YELLOW12:9 for L1 being Semilattice for L2 being non empty RelStr for x, y being Element of L1 for x1, y1 being Element of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & x = x1 & y = y1 holds x "/\" y = x1 "/\" y1 proof let L1 be Semilattice; ::_thesis: for L2 being non empty RelStr for x, y being Element of L1 for x1, y1 being Element of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & x = x1 & y = y1 holds x "/\" y = x1 "/\" y1 let L2 be non empty RelStr ; ::_thesis: for x, y being Element of L1 for x1, y1 being Element of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & x = x1 & y = y1 holds x "/\" y = x1 "/\" y1 let x, y be Element of L1; ::_thesis: for x1, y1 being Element of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & x = x1 & y = y1 holds x "/\" y = x1 "/\" y1 let x1, y1 be Element of L2; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & x = x1 & y = y1 implies x "/\" y = x1 "/\" y1 ) assume that A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and A2: ( x = x1 & y = y1 ) ; ::_thesis: x "/\" y = x1 "/\" y1 A3: L2 is with_infima Poset by A1, WAYBEL_8:12, WAYBEL_8:13, WAYBEL_8:14, YELLOW_7:14; A4: ex_inf_of {x,y},L1 by YELLOW_0:21; thus x "/\" y = inf {x,y} by YELLOW_0:40 .= inf {x1,y1} by A1, A2, A4, YELLOW_0:27 .= x1 "/\" y1 by A3, YELLOW_0:40 ; ::_thesis: verum end; theorem Th10: :: YELLOW12:10 for L1 being sup-Semilattice for L2 being non empty RelStr for x, y being Element of L1 for x1, y1 being Element of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & x = x1 & y = y1 holds x "\/" y = x1 "\/" y1 proof let L1 be sup-Semilattice; ::_thesis: for L2 being non empty RelStr for x, y being Element of L1 for x1, y1 being Element of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & x = x1 & y = y1 holds x "\/" y = x1 "\/" y1 let L2 be non empty RelStr ; ::_thesis: for x, y being Element of L1 for x1, y1 being Element of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & x = x1 & y = y1 holds x "\/" y = x1 "\/" y1 let x, y be Element of L1; ::_thesis: for x1, y1 being Element of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & x = x1 & y = y1 holds x "\/" y = x1 "\/" y1 let x1, y1 be Element of L2; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & x = x1 & y = y1 implies x "\/" y = x1 "\/" y1 ) assume that A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and A2: ( x = x1 & y = y1 ) ; ::_thesis: x "\/" y = x1 "\/" y1 A3: L2 is with_suprema Poset by A1, WAYBEL_8:12, WAYBEL_8:13, WAYBEL_8:14, YELLOW_7:15; A4: ex_sup_of {x,y},L1 by YELLOW_0:20; thus x "\/" y = sup {x,y} by YELLOW_0:41 .= sup {x1,y1} by A1, A2, A4, YELLOW_0:26 .= x1 "\/" y1 by A3, YELLOW_0:41 ; ::_thesis: verum end; theorem Th11: :: YELLOW12:11 for L1 being Semilattice for L2 being non empty RelStr for X, Y being Subset of L1 for X1, Y1 being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = X1 & Y = Y1 holds X "/\" Y = X1 "/\" Y1 proof let L1 be Semilattice; ::_thesis: for L2 being non empty RelStr for X, Y being Subset of L1 for X1, Y1 being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = X1 & Y = Y1 holds X "/\" Y = X1 "/\" Y1 let L2 be non empty RelStr ; ::_thesis: for X, Y being Subset of L1 for X1, Y1 being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = X1 & Y = Y1 holds X "/\" Y = X1 "/\" Y1 let X, Y be Subset of L1; ::_thesis: for X1, Y1 being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = X1 & Y = Y1 holds X "/\" Y = X1 "/\" Y1 let X1, Y1 be Subset of L2; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = X1 & Y = Y1 implies X "/\" Y = X1 "/\" Y1 ) assume that A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and A2: ( X = X1 & Y = Y1 ) ; ::_thesis: X "/\" Y = X1 "/\" Y1 set XY = { (x "/\" y) where x, y is Element of L1 : ( x in X & y in Y ) } ; set XY1 = { (x "/\" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) } ; A3: { (x "/\" y) where x, y is Element of L1 : ( x in X & y in Y ) } = { (x "/\" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) } proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { (x "/\" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) } c= { (x "/\" y) where x, y is Element of L1 : ( x in X & y in Y ) } let a be set ; ::_thesis: ( a in { (x "/\" y) where x, y is Element of L1 : ( x in X & y in Y ) } implies a in { (x "/\" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) } ) assume a in { (x "/\" y) where x, y is Element of L1 : ( x in X & y in Y ) } ; ::_thesis: a in { (x "/\" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) } then consider x, y being Element of L1 such that A4: a = x "/\" y and A5: ( x in X & y in Y ) ; reconsider x1 = x, y1 = y as Element of L2 by A1; a = x1 "/\" y1 by A1, A4, Th9; hence a in { (x "/\" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) } by A2, A5; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (x "/\" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) } or a in { (x "/\" y) where x, y is Element of L1 : ( x in X & y in Y ) } ) assume a in { (x "/\" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) } ; ::_thesis: a in { (x "/\" y) where x, y is Element of L1 : ( x in X & y in Y ) } then consider x, y being Element of L2 such that A6: a = x "/\" y and A7: ( x in X1 & y in Y1 ) ; reconsider x1 = x, y1 = y as Element of L1 by A1; a = x1 "/\" y1 by A1, A6, Th9; hence a in { (x "/\" y) where x, y is Element of L1 : ( x in X & y in Y ) } by A2, A7; ::_thesis: verum end; thus X "/\" Y = { (x "/\" y) where x, y is Element of L1 : ( x in X & y in Y ) } by YELLOW_4:def_4 .= X1 "/\" Y1 by A3, YELLOW_4:def_4 ; ::_thesis: verum end; theorem :: YELLOW12:12 for L1 being sup-Semilattice for L2 being non empty RelStr for X, Y being Subset of L1 for X1, Y1 being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = X1 & Y = Y1 holds X "\/" Y = X1 "\/" Y1 proof let L1 be sup-Semilattice; ::_thesis: for L2 being non empty RelStr for X, Y being Subset of L1 for X1, Y1 being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = X1 & Y = Y1 holds X "\/" Y = X1 "\/" Y1 let L2 be non empty RelStr ; ::_thesis: for X, Y being Subset of L1 for X1, Y1 being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = X1 & Y = Y1 holds X "\/" Y = X1 "\/" Y1 let X, Y be Subset of L1; ::_thesis: for X1, Y1 being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = X1 & Y = Y1 holds X "\/" Y = X1 "\/" Y1 let X1, Y1 be Subset of L2; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = X1 & Y = Y1 implies X "\/" Y = X1 "\/" Y1 ) assume that A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and A2: ( X = X1 & Y = Y1 ) ; ::_thesis: X "\/" Y = X1 "\/" Y1 set XY = { (x "\/" y) where x, y is Element of L1 : ( x in X & y in Y ) } ; set XY1 = { (x "\/" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) } ; A3: { (x "\/" y) where x, y is Element of L1 : ( x in X & y in Y ) } = { (x "\/" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) } proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { (x "\/" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) } c= { (x "\/" y) where x, y is Element of L1 : ( x in X & y in Y ) } let a be set ; ::_thesis: ( a in { (x "\/" y) where x, y is Element of L1 : ( x in X & y in Y ) } implies a in { (x "\/" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) } ) assume a in { (x "\/" y) where x, y is Element of L1 : ( x in X & y in Y ) } ; ::_thesis: a in { (x "\/" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) } then consider x, y being Element of L1 such that A4: a = x "\/" y and A5: ( x in X & y in Y ) ; reconsider x1 = x, y1 = y as Element of L2 by A1; a = x1 "\/" y1 by A1, A4, Th10; hence a in { (x "\/" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) } by A2, A5; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (x "\/" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) } or a in { (x "\/" y) where x, y is Element of L1 : ( x in X & y in Y ) } ) assume a in { (x "\/" y) where x, y is Element of L2 : ( x in X1 & y in Y1 ) } ; ::_thesis: a in { (x "\/" y) where x, y is Element of L1 : ( x in X & y in Y ) } then consider x, y being Element of L2 such that A6: a = x "\/" y and A7: ( x in X1 & y in Y1 ) ; reconsider x1 = x, y1 = y as Element of L1 by A1; a = x1 "\/" y1 by A1, A6, Th10; hence a in { (x "\/" y) where x, y is Element of L1 : ( x in X & y in Y ) } by A2, A7; ::_thesis: verum end; thus X "\/" Y = { (x "\/" y) where x, y is Element of L1 : ( x in X & y in Y ) } by YELLOW_4:def_3 .= X1 "\/" Y1 by A3, YELLOW_4:def_3 ; ::_thesis: verum end; theorem Th13: :: YELLOW12:13 for L1 being non empty reflexive antisymmetric up-complete RelStr for L2 being non empty reflexive RelStr for x being Element of L1 for y being Element of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & x = y holds ( waybelow x = waybelow y & wayabove x = wayabove y ) proof let L1 be non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: for L2 being non empty reflexive RelStr for x being Element of L1 for y being Element of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & x = y holds ( waybelow x = waybelow y & wayabove x = wayabove y ) let L2 be non empty reflexive RelStr ; ::_thesis: for x being Element of L1 for y being Element of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & x = y holds ( waybelow x = waybelow y & wayabove x = wayabove y ) let x be Element of L1; ::_thesis: for y being Element of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & x = y holds ( waybelow x = waybelow y & wayabove x = wayabove y ) let y be Element of L2; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & x = y implies ( waybelow x = waybelow y & wayabove x = wayabove y ) ) assume that A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and A2: x = y ; ::_thesis: ( waybelow x = waybelow y & wayabove x = wayabove y ) hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: wayabove x = wayabove y hereby ::_thesis: for a being set st a in waybelow y holds a in waybelow x let a be set ; ::_thesis: ( a in waybelow x implies a in waybelow y ) assume a in waybelow x ; ::_thesis: a in waybelow y then consider z being Element of L1 such that A3: a = z and A4: z << x ; reconsider w = z as Element of L2 by A1; L2 is antisymmetric by A1, WAYBEL_8:14; then w << y by A1, A2, A4, WAYBEL_8:8; hence a in waybelow y by A3; ::_thesis: verum end; let a be set ; ::_thesis: ( a in waybelow y implies a in waybelow x ) assume a in waybelow y ; ::_thesis: a in waybelow x then consider z being Element of L2 such that A5: a = z and A6: z << y ; reconsider w = z as Element of L1 by A1; ( L2 is up-complete & L2 is antisymmetric ) by A1, WAYBEL_8:14, WAYBEL_8:15; then w << x by A1, A2, A6, WAYBEL_8:8; hence a in waybelow x by A5; ::_thesis: verum end; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: wayabove y c= wayabove x let a be set ; ::_thesis: ( a in wayabove x implies a in wayabove y ) assume a in wayabove x ; ::_thesis: a in wayabove y then consider z being Element of L1 such that A7: a = z and A8: z >> x ; reconsider w = z as Element of L2 by A1; L2 is antisymmetric by A1, WAYBEL_8:14; then w >> y by A1, A2, A8, WAYBEL_8:8; hence a in wayabove y by A7; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in wayabove y or a in wayabove x ) assume a in wayabove y ; ::_thesis: a in wayabove x then consider z being Element of L2 such that A9: a = z and A10: z >> y ; reconsider w = z as Element of L1 by A1; ( L2 is up-complete & L2 is antisymmetric ) by A1, WAYBEL_8:14, WAYBEL_8:15; then w >> x by A1, A2, A10, WAYBEL_8:8; hence a in wayabove x by A9; ::_thesis: verum end; theorem :: YELLOW12:14 for L1 being meet-continuous Semilattice for L2 being non empty reflexive RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds L2 is meet-continuous proof let L1 be meet-continuous Semilattice; ::_thesis: for L2 being non empty reflexive RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds L2 is meet-continuous let L2 be non empty reflexive RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies L2 is meet-continuous ) assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: L2 is meet-continuous hence L2 is up-complete by WAYBEL_8:15; :: according to WAYBEL_2:def_7 ::_thesis: L2 is satisfying_MC let x be Element of L2; :: according to WAYBEL_2:def_6 ::_thesis: for b1 being Element of bool the carrier of L2 holds x "/\" ("\/" (b1,L2)) = "\/" (({x} "/\" b1),L2) let D be non empty directed Subset of L2; ::_thesis: x "/\" ("\/" (D,L2)) = "\/" (({x} "/\" D),L2) reconsider E = D as non empty directed Subset of L1 by A1, WAYBEL_0:3; reconsider y = x as Element of L1 by A1; A2: {x} "/\" D = {y} "/\" E by A1, Th11; reconsider yy = {y} as non empty directed Subset of L1 by WAYBEL_0:5; A3: ex_sup_of yy "/\" E,L1 by WAYBEL_0:75; ex_sup_of E,L1 by WAYBEL_0:75; then sup D = sup E by A1, YELLOW_0:26; hence x "/\" (sup D) = y "/\" (sup E) by A1, Th9 .= sup ({y} "/\" E) by WAYBEL_2:def_6 .= sup ({x} "/\" D) by A1, A2, A3, YELLOW_0:26 ; ::_thesis: verum end; theorem :: YELLOW12:15 for L1 being non empty reflexive antisymmetric continuous RelStr for L2 being non empty reflexive RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds L2 is continuous proof let L1 be non empty reflexive antisymmetric continuous RelStr ; ::_thesis: for L2 being non empty reflexive RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) holds L2 is continuous let L2 be non empty reflexive RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies L2 is continuous ) assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; ::_thesis: L2 is continuous hereby :: according to WAYBEL_3:def_6 ::_thesis: ( L2 is up-complete & L2 is satisfying_axiom_of_approximation ) let y be Element of L2; ::_thesis: ( not waybelow y is empty & waybelow y is directed ) reconsider x = y as Element of L1 by A1; waybelow x = waybelow y by A1, Th13; hence ( not waybelow y is empty & waybelow y is directed ) by A1, WAYBEL_0:3; ::_thesis: verum end; thus L2 is up-complete by A1, WAYBEL_8:15; ::_thesis: L2 is satisfying_axiom_of_approximation let y be Element of L2; :: according to WAYBEL_3:def_5 ::_thesis: y = "\/" ((waybelow y),L2) reconsider x = y as Element of L1 by A1; A2: ( ex_sup_of waybelow x,L1 & x = sup (waybelow x) ) by WAYBEL_0:75, WAYBEL_3:def_5; waybelow x = waybelow y by A1, Th13; hence y = "\/" ((waybelow y),L2) by A1, A2, YELLOW_0:26; ::_thesis: verum end; theorem :: YELLOW12:16 for L1, L2 being RelStr for A being Subset of L1 for J being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & A = J holds subrelstr A = subrelstr J proof let L1, L2 be RelStr ; ::_thesis: for A being Subset of L1 for J being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & A = J holds subrelstr A = subrelstr J let A be Subset of L1; ::_thesis: for J being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & A = J holds subrelstr A = subrelstr J let J be Subset of L2; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & A = J implies subrelstr A = subrelstr J ) assume that A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and A2: A = J ; ::_thesis: subrelstr A = subrelstr J A3: the carrier of (subrelstr A) = A by YELLOW_0:def_15 .= the carrier of (subrelstr J) by A2, YELLOW_0:def_15 ; then the InternalRel of (subrelstr A) = the InternalRel of L2 |_2 the carrier of (subrelstr J) by A1, YELLOW_0:def_14 .= the InternalRel of (subrelstr J) by YELLOW_0:def_14 ; hence subrelstr A = subrelstr J by A3; ::_thesis: verum end; theorem :: YELLOW12:17 for L1, L2 being non empty RelStr for A being SubRelStr of L1 for J being SubRelStr of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of J, the InternalRel of J #) & A is meet-inheriting holds J is meet-inheriting proof let L1, L2 be non empty RelStr ; ::_thesis: for A being SubRelStr of L1 for J being SubRelStr of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of J, the InternalRel of J #) & A is meet-inheriting holds J is meet-inheriting let A be SubRelStr of L1; ::_thesis: for J being SubRelStr of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of J, the InternalRel of J #) & A is meet-inheriting holds J is meet-inheriting let J be SubRelStr of L2; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of J, the InternalRel of J #) & A is meet-inheriting implies J is meet-inheriting ) assume that A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and A2: RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of J, the InternalRel of J #) and A3: for x, y being Element of L1 st x in the carrier of A & y in the carrier of A & ex_inf_of {x,y},L1 holds inf {x,y} in the carrier of A ; :: according to YELLOW_0:def_16 ::_thesis: J is meet-inheriting let x, y be Element of L2; :: according to YELLOW_0:def_16 ::_thesis: ( not x in the carrier of J or not y in the carrier of J or not ex_inf_of {x,y},L2 or "/\" ({x,y},L2) in the carrier of J ) assume that A4: ( x in the carrier of J & y in the carrier of J ) and A5: ex_inf_of {x,y},L2 ; ::_thesis: "/\" ({x,y},L2) in the carrier of J reconsider x1 = x, y1 = y as Element of L1 by A1; inf {x1,y1} in the carrier of A by A1, A2, A3, A4, A5, YELLOW_0:14; hence "/\" ({x,y},L2) in the carrier of J by A1, A2, A5, YELLOW_0:27; ::_thesis: verum end; theorem :: YELLOW12:18 for L1, L2 being non empty RelStr for A being SubRelStr of L1 for J being SubRelStr of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of J, the InternalRel of J #) & A is join-inheriting holds J is join-inheriting proof let L1, L2 be non empty RelStr ; ::_thesis: for A being SubRelStr of L1 for J being SubRelStr of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of J, the InternalRel of J #) & A is join-inheriting holds J is join-inheriting let A be SubRelStr of L1; ::_thesis: for J being SubRelStr of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of J, the InternalRel of J #) & A is join-inheriting holds J is join-inheriting let J be SubRelStr of L2; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of J, the InternalRel of J #) & A is join-inheriting implies J is join-inheriting ) assume that A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and A2: RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of J, the InternalRel of J #) and A3: for x, y being Element of L1 st x in the carrier of A & y in the carrier of A & ex_sup_of {x,y},L1 holds sup {x,y} in the carrier of A ; :: according to YELLOW_0:def_17 ::_thesis: J is join-inheriting let x, y be Element of L2; :: according to YELLOW_0:def_17 ::_thesis: ( not x in the carrier of J or not y in the carrier of J or not ex_sup_of {x,y},L2 or "\/" ({x,y},L2) in the carrier of J ) assume that A4: ( x in the carrier of J & y in the carrier of J ) and A5: ex_sup_of {x,y},L2 ; ::_thesis: "\/" ({x,y},L2) in the carrier of J reconsider x1 = x, y1 = y as Element of L1 by A1; sup {x1,y1} in the carrier of A by A1, A2, A3, A4, A5, YELLOW_0:14; hence "\/" ({x,y},L2) in the carrier of J by A1, A2, A5, YELLOW_0:26; ::_thesis: verum end; theorem :: YELLOW12:19 for L1 being non empty reflexive antisymmetric up-complete RelStr for L2 being non empty reflexive RelStr for X being Subset of L1 for Y being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = Y & X is property(S) holds Y is property(S) proof let L1 be non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: for L2 being non empty reflexive RelStr for X being Subset of L1 for Y being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = Y & X is property(S) holds Y is property(S) let L2 be non empty reflexive RelStr ; ::_thesis: for X being Subset of L1 for Y being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = Y & X is property(S) holds Y is property(S) let X be Subset of L1; ::_thesis: for Y being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = Y & X is property(S) holds Y is property(S) let Y be Subset of L2; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = Y & X is property(S) implies Y is property(S) ) assume that A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and A2: X = Y and A3: for D being non empty directed Subset of L1 st sup D in X holds ex y being Element of L1 st ( y in D & ( for x being Element of L1 st x in D & x >= y holds x in X ) ) ; :: according to WAYBEL11:def_3 ::_thesis: Y is property(S) let E be non empty directed Subset of L2; :: according to WAYBEL11:def_3 ::_thesis: ( not "\/" (E,L2) in Y or ex b1 being Element of the carrier of L2 st ( b1 in E & ( for b2 being Element of the carrier of L2 holds ( not b2 in E or not b1 <= b2 or b2 in Y ) ) ) ) assume A4: sup E in Y ; ::_thesis: ex b1 being Element of the carrier of L2 st ( b1 in E & ( for b2 being Element of the carrier of L2 holds ( not b2 in E or not b1 <= b2 or b2 in Y ) ) ) reconsider D = E as non empty directed Subset of L1 by A1, WAYBEL_0:3; ex_sup_of D,L1 by WAYBEL_0:75; then sup D in X by A1, A2, A4, YELLOW_0:26; then consider y being Element of L1 such that A5: y in D and A6: for x being Element of L1 st x in D & x >= y holds x in X by A3; reconsider y2 = y as Element of L2 by A1; take y2 ; ::_thesis: ( y2 in E & ( for b1 being Element of the carrier of L2 holds ( not b1 in E or not y2 <= b1 or b1 in Y ) ) ) thus y2 in E by A5; ::_thesis: for b1 being Element of the carrier of L2 holds ( not b1 in E or not y2 <= b1 or b1 in Y ) let x2 be Element of L2; ::_thesis: ( not x2 in E or not y2 <= x2 or x2 in Y ) assume ( x2 in E & x2 >= y2 ) ; ::_thesis: x2 in Y hence x2 in Y by A1, A2, A6, YELLOW_0:1; ::_thesis: verum end; theorem :: YELLOW12:20 for L1 being non empty reflexive antisymmetric up-complete RelStr for L2 being non empty reflexive RelStr for X being Subset of L1 for Y being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = Y & X is directly_closed holds Y is directly_closed proof let L1 be non empty reflexive antisymmetric up-complete RelStr ; ::_thesis: for L2 being non empty reflexive RelStr for X being Subset of L1 for Y being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = Y & X is directly_closed holds Y is directly_closed let L2 be non empty reflexive RelStr ; ::_thesis: for X being Subset of L1 for Y being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = Y & X is directly_closed holds Y is directly_closed let X be Subset of L1; ::_thesis: for Y being Subset of L2 st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = Y & X is directly_closed holds Y is directly_closed let Y be Subset of L2; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & X = Y & X is directly_closed implies Y is directly_closed ) assume that A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and A2: X = Y and A3: for D being non empty directed Subset of L1 st D c= X holds sup D in X ; :: according to WAYBEL11:def_2 ::_thesis: Y is directly_closed let E be non empty directed Subset of L2; :: according to WAYBEL11:def_2 ::_thesis: ( not E c= Y or "\/" (E,L2) in Y ) assume A4: E c= Y ; ::_thesis: "\/" (E,L2) in Y reconsider D = E as non empty directed Subset of L1 by A1, WAYBEL_0:3; ( ex_sup_of D,L1 & sup D in X ) by A2, A3, A4, WAYBEL_0:75; hence "\/" (E,L2) in Y by A1, A2, YELLOW_0:26; ::_thesis: verum end; theorem :: YELLOW12:21 for N being antisymmetric with_infima RelStr for D, E being Subset of N for X being upper Subset of N st D misses X holds D "/\" E misses X proof let N be antisymmetric with_infima RelStr ; ::_thesis: for D, E being Subset of N for X being upper Subset of N st D misses X holds D "/\" E misses X let D, E be Subset of N; ::_thesis: for X being upper Subset of N st D misses X holds D "/\" E misses X let X be upper Subset of N; ::_thesis: ( D misses X implies D "/\" E misses X ) assume A1: D /\ X = {} ; :: according to XBOOLE_0:def_7 ::_thesis: D "/\" E misses X assume (D "/\" E) /\ X <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then consider k being set such that A2: k in (D "/\" E) /\ X by XBOOLE_0:def_1; reconsider k = k as Element of N by A2; A3: ( D "/\" E = { (d "/\" e) where d, e is Element of N : ( d in D & e in E ) } & k in D "/\" E ) by A2, XBOOLE_0:def_4, YELLOW_4:def_4; A4: k in X by A2, XBOOLE_0:def_4; consider d, e being Element of N such that A5: k = d "/\" e and A6: d in D and e in E by A3; d "/\" e <= d by YELLOW_0:23; then d in X by A4, A5, WAYBEL_0:def_20; hence contradiction by A1, A6, XBOOLE_0:def_4; ::_thesis: verum end; theorem :: YELLOW12:22 for R being non empty reflexive RelStr holds id the carrier of R c= the InternalRel of R /\ the InternalRel of (R ~) proof let R be non empty reflexive RelStr ; ::_thesis: id the carrier of R c= the InternalRel of R /\ the InternalRel of (R ~) let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in id the carrier of R or a in the InternalRel of R /\ the InternalRel of (R ~) ) assume A1: a in id the carrier of R ; ::_thesis: a in the InternalRel of R /\ the InternalRel of (R ~) then consider y, z being set such that A2: a = [y,z] by RELAT_1:def_1; reconsider y = y, z = z as Element of R by A1, A2, ZFMISC_1:87; y <= z by A1, A2, RELAT_1:def_10; then A3: a in the InternalRel of R by A2, ORDERS_2:def_5; y = z by A1, A2, RELAT_1:def_10; then a in the InternalRel of (R ~) by A2, A3, RELAT_1:def_7; hence a in the InternalRel of R /\ the InternalRel of (R ~) by A3, XBOOLE_0:def_4; ::_thesis: verum end; theorem :: YELLOW12:23 for R being antisymmetric RelStr holds the InternalRel of R /\ the InternalRel of (R ~) c= id the carrier of R proof let R be antisymmetric RelStr ; ::_thesis: the InternalRel of R /\ the InternalRel of (R ~) c= id the carrier of R let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the InternalRel of R /\ the InternalRel of (R ~) or a in id the carrier of R ) assume A1: a in the InternalRel of R /\ the InternalRel of (R ~) ; ::_thesis: a in id the carrier of R then consider y, z being set such that A2: a = [y,z] by RELAT_1:def_1; A3: y in the carrier of R by A1, A2, ZFMISC_1:87; reconsider y = y, z = z as Element of R by A1, A2, ZFMISC_1:87; a in the InternalRel of (R ~) by A1, XBOOLE_0:def_4; then [z,y] in the InternalRel of R by A2, RELAT_1:def_7; then A4: z <= y by ORDERS_2:def_5; a in the InternalRel of R by A1, XBOOLE_0:def_4; then y <= z by A2, ORDERS_2:def_5; then y = z by A4, ORDERS_2:2; hence a in id the carrier of R by A2, A3, RELAT_1:def_10; ::_thesis: verum end; definition let L be non empty RelStr ; let f be Function of [:L,L:],L; let a, b be Element of L; :: original: . redefine funcf . (a,b) -> Element of L; coherence f . (a,b) is Element of L proof f . [a,b] is Element of L ; hence f . (a,b) is Element of L ; ::_thesis: verum end; end; theorem Th24: :: YELLOW12:24 for R being upper-bounded Semilattice for X being Subset of [:R,R:] st ex_inf_of (inf_op R) .: X,R holds inf_op R preserves_inf_of X proof let R be upper-bounded Semilattice; ::_thesis: for X being Subset of [:R,R:] st ex_inf_of (inf_op R) .: X,R holds inf_op R preserves_inf_of X set f = inf_op R; let X be Subset of [:R,R:]; ::_thesis: ( ex_inf_of (inf_op R) .: X,R implies inf_op R preserves_inf_of X ) assume that A1: ex_inf_of (inf_op R) .: X,R and A2: ex_inf_of X,[:R,R:] ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of (inf_op R) .: X,R & "/\" (((inf_op R) .: X),R) = (inf_op R) . ("/\" (X,[:R,R:])) ) thus ex_inf_of (inf_op R) .: X,R by A1; ::_thesis: "/\" (((inf_op R) .: X),R) = (inf_op R) . ("/\" (X,[:R,R:])) A3: dom (inf_op R) = the carrier of [:R,R:] by FUNCT_2:def_1; then A4: dom (inf_op R) = [: the carrier of R, the carrier of R:] by YELLOW_3:def_2; A5: for b being Element of R st b is_<=_than (inf_op R) .: X holds (inf_op R) . (inf X) >= b proof let b be Element of R; ::_thesis: ( b is_<=_than (inf_op R) .: X implies (inf_op R) . (inf X) >= b ) assume A6: b is_<=_than (inf_op R) .: X ; ::_thesis: (inf_op R) . (inf X) >= b X is_>=_than [b,b] proof let c be Element of [:R,R:]; :: according to LATTICE3:def_8 ::_thesis: ( not c in X or [b,b] <= c ) assume c in X ; ::_thesis: [b,b] <= c then (inf_op R) . c in (inf_op R) .: X by A3, FUNCT_1:def_6; then A7: b <= (inf_op R) . c by A6, LATTICE3:def_8; consider s, t being set such that A8: ( s in the carrier of R & t in the carrier of R ) and A9: c = [s,t] by A3, A4, ZFMISC_1:def_2; reconsider s = s, t = t as Element of R by A8; A10: (inf_op R) . c = (inf_op R) . (s,t) by A9 .= s "/\" t by WAYBEL_2:def_4 ; s "/\" t <= t by YELLOW_0:23; then A11: b <= t by A7, A10, ORDERS_2:3; s "/\" t <= s by YELLOW_0:23; then b <= s by A7, A10, ORDERS_2:3; hence [b,b] <= c by A9, A11, YELLOW_3:11; ::_thesis: verum end; then [b,b] <= inf X by A2, YELLOW_0:def_10; then (inf_op R) . (b,b) <= (inf_op R) . (inf X) by WAYBEL_1:def_2; then b "/\" b <= (inf_op R) . (inf X) by WAYBEL_2:def_4; hence b <= (inf_op R) . (inf X) by YELLOW_0:25; ::_thesis: verum end; inf X is_<=_than X by A2, YELLOW_0:def_10; then (inf_op R) . (inf X) is_<=_than (inf_op R) .: X by YELLOW_2:13; hence "/\" (((inf_op R) .: X),R) = (inf_op R) . ("/\" (X,[:R,R:])) by A1, A5, YELLOW_0:def_10; ::_thesis: verum end; registration let R be complete Semilattice; cluster inf_op R -> infs-preserving ; coherence inf_op R is infs-preserving proof let X be Subset of [:R,R:]; :: according to WAYBEL_0:def_32 ::_thesis: inf_op R preserves_inf_of X assume A1: ex_inf_of X,[:R,R:] ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of (inf_op R) .: X,R & "/\" (((inf_op R) .: X),R) = (inf_op R) . ("/\" (X,[:R,R:])) ) thus ex_inf_of (inf_op R) .: X,R by YELLOW_0:17; ::_thesis: "/\" (((inf_op R) .: X),R) = (inf_op R) . ("/\" (X,[:R,R:])) then inf_op R preserves_inf_of X by Th24; hence "/\" (((inf_op R) .: X),R) = (inf_op R) . ("/\" (X,[:R,R:])) by A1, WAYBEL_0:def_30; ::_thesis: verum end; end; theorem Th25: :: YELLOW12:25 for R being lower-bounded sup-Semilattice for X being Subset of [:R,R:] st ex_sup_of (sup_op R) .: X,R holds sup_op R preserves_sup_of X proof let R be lower-bounded sup-Semilattice; ::_thesis: for X being Subset of [:R,R:] st ex_sup_of (sup_op R) .: X,R holds sup_op R preserves_sup_of X set f = sup_op R; let X be Subset of [:R,R:]; ::_thesis: ( ex_sup_of (sup_op R) .: X,R implies sup_op R preserves_sup_of X ) assume that A1: ex_sup_of (sup_op R) .: X,R and A2: ex_sup_of X,[:R,R:] ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (sup_op R) .: X,R & "\/" (((sup_op R) .: X),R) = (sup_op R) . ("\/" (X,[:R,R:])) ) thus ex_sup_of (sup_op R) .: X,R by A1; ::_thesis: "\/" (((sup_op R) .: X),R) = (sup_op R) . ("\/" (X,[:R,R:])) A3: dom (sup_op R) = the carrier of [:R,R:] by FUNCT_2:def_1; then A4: dom (sup_op R) = [: the carrier of R, the carrier of R:] by YELLOW_3:def_2; A5: for b being Element of R st b is_>=_than (sup_op R) .: X holds (sup_op R) . (sup X) <= b proof let b be Element of R; ::_thesis: ( b is_>=_than (sup_op R) .: X implies (sup_op R) . (sup X) <= b ) assume A6: b is_>=_than (sup_op R) .: X ; ::_thesis: (sup_op R) . (sup X) <= b X is_<=_than [b,b] proof let c be Element of [:R,R:]; :: according to LATTICE3:def_9 ::_thesis: ( not c in X or c <= [b,b] ) assume c in X ; ::_thesis: c <= [b,b] then (sup_op R) . c in (sup_op R) .: X by A3, FUNCT_1:def_6; then A7: (sup_op R) . c <= b by A6, LATTICE3:def_9; consider s, t being set such that A8: ( s in the carrier of R & t in the carrier of R ) and A9: c = [s,t] by A3, A4, ZFMISC_1:def_2; reconsider s = s, t = t as Element of R by A8; A10: (sup_op R) . c = (sup_op R) . (s,t) by A9 .= s "\/" t by WAYBEL_2:def_5 ; t <= s "\/" t by YELLOW_0:22; then A11: t <= b by A7, A10, ORDERS_2:3; s <= s "\/" t by YELLOW_0:22; then s <= b by A7, A10, ORDERS_2:3; hence c <= [b,b] by A9, A11, YELLOW_3:11; ::_thesis: verum end; then sup X <= [b,b] by A2, YELLOW_0:def_9; then (sup_op R) . (sup X) <= (sup_op R) . (b,b) by WAYBEL_1:def_2; then ( b <= b & (sup_op R) . (sup X) <= b "\/" b ) by WAYBEL_2:def_5; hence (sup_op R) . (sup X) <= b by YELLOW_0:24; ::_thesis: verum end; X is_<=_than sup X by A2, YELLOW_0:def_9; then (sup_op R) .: X is_<=_than (sup_op R) . (sup X) by YELLOW_2:14; hence "\/" (((sup_op R) .: X),R) = (sup_op R) . ("\/" (X,[:R,R:])) by A1, A5, YELLOW_0:def_9; ::_thesis: verum end; registration let R be complete sup-Semilattice; cluster sup_op R -> sups-preserving ; coherence sup_op R is sups-preserving proof let X be Subset of [:R,R:]; :: according to WAYBEL_0:def_33 ::_thesis: sup_op R preserves_sup_of X assume A1: ex_sup_of X,[:R,R:] ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (sup_op R) .: X,R & "\/" (((sup_op R) .: X),R) = (sup_op R) . ("\/" (X,[:R,R:])) ) thus ex_sup_of (sup_op R) .: X,R by YELLOW_0:17; ::_thesis: "\/" (((sup_op R) .: X),R) = (sup_op R) . ("\/" (X,[:R,R:])) then sup_op R preserves_sup_of X by Th25; hence "\/" (((sup_op R) .: X),R) = (sup_op R) . ("\/" (X,[:R,R:])) by A1, WAYBEL_0:def_31; ::_thesis: verum end; end; theorem :: YELLOW12:26 for N being Semilattice for A being Subset of N st subrelstr A is meet-inheriting holds A is filtered proof let N be Semilattice; ::_thesis: for A being Subset of N st subrelstr A is meet-inheriting holds A is filtered let A be Subset of N; ::_thesis: ( subrelstr A is meet-inheriting implies A is filtered ) assume A1: subrelstr A is meet-inheriting ; ::_thesis: A is filtered let x, y be Element of N; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in A or not y in A or ex b1 being Element of the carrier of N st ( b1 in A & b1 <= x & b1 <= y ) ) assume A2: ( x in A & y in A ) ; ::_thesis: ex b1 being Element of the carrier of N st ( b1 in A & b1 <= x & b1 <= y ) take x "/\" y ; ::_thesis: ( x "/\" y in A & x "/\" y <= x & x "/\" y <= y ) A3: the carrier of (subrelstr A) = A by YELLOW_0:def_15; ex_inf_of {x,y},N by YELLOW_0:21; then inf {x,y} in the carrier of (subrelstr A) by A1, A2, A3, YELLOW_0:def_16; hence x "/\" y in A by A3, YELLOW_0:40; ::_thesis: ( x "/\" y <= x & x "/\" y <= y ) thus ( x "/\" y <= x & x "/\" y <= y ) by YELLOW_0:23; ::_thesis: verum end; theorem :: YELLOW12:27 for N being sup-Semilattice for A being Subset of N st subrelstr A is join-inheriting holds A is directed proof let N be sup-Semilattice; ::_thesis: for A being Subset of N st subrelstr A is join-inheriting holds A is directed let A be Subset of N; ::_thesis: ( subrelstr A is join-inheriting implies A is directed ) assume A1: subrelstr A is join-inheriting ; ::_thesis: A is directed let x, y be Element of N; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in A or not y in A or ex b1 being Element of the carrier of N st ( b1 in A & x <= b1 & y <= b1 ) ) assume A2: ( x in A & y in A ) ; ::_thesis: ex b1 being Element of the carrier of N st ( b1 in A & x <= b1 & y <= b1 ) take x "\/" y ; ::_thesis: ( x "\/" y in A & x <= x "\/" y & y <= x "\/" y ) A3: the carrier of (subrelstr A) = A by YELLOW_0:def_15; ex_sup_of {x,y},N by YELLOW_0:20; then sup {x,y} in the carrier of (subrelstr A) by A1, A2, A3, YELLOW_0:def_17; hence x "\/" y in A by A3, YELLOW_0:41; ::_thesis: ( x <= x "\/" y & y <= x "\/" y ) thus ( x <= x "\/" y & y <= x "\/" y ) by YELLOW_0:22; ::_thesis: verum end; theorem :: YELLOW12:28 for N being transitive RelStr for A, J being Subset of N st A is_coarser_than uparrow J holds uparrow A c= uparrow J proof let N be transitive RelStr ; ::_thesis: for A, J being Subset of N st A is_coarser_than uparrow J holds uparrow A c= uparrow J let A, J be Subset of N; ::_thesis: ( A is_coarser_than uparrow J implies uparrow A c= uparrow J ) assume A1: A is_coarser_than uparrow J ; ::_thesis: uparrow A c= uparrow J let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in uparrow A or w in uparrow J ) assume A2: w in uparrow A ; ::_thesis: w in uparrow J then reconsider w1 = w as Element of N ; consider t being Element of N such that A3: t <= w1 and A4: t in A by A2, WAYBEL_0:def_16; consider t1 being Element of N such that A5: t1 in uparrow J and A6: t1 <= t by A1, A4, YELLOW_4:def_2; consider t2 being Element of N such that A7: t2 <= t1 and A8: t2 in J by A5, WAYBEL_0:def_16; t2 <= t by A6, A7, ORDERS_2:3; then t2 <= w1 by A3, ORDERS_2:3; hence w in uparrow J by A8, WAYBEL_0:def_16; ::_thesis: verum end; theorem :: YELLOW12:29 for N being transitive RelStr for A, J being Subset of N st A is_finer_than downarrow J holds downarrow A c= downarrow J proof let N be transitive RelStr ; ::_thesis: for A, J being Subset of N st A is_finer_than downarrow J holds downarrow A c= downarrow J let A, J be Subset of N; ::_thesis: ( A is_finer_than downarrow J implies downarrow A c= downarrow J ) assume A1: A is_finer_than downarrow J ; ::_thesis: downarrow A c= downarrow J let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in downarrow A or w in downarrow J ) assume A2: w in downarrow A ; ::_thesis: w in downarrow J then reconsider w1 = w as Element of N ; consider t being Element of N such that A3: w1 <= t and A4: t in A by A2, WAYBEL_0:def_15; consider t1 being Element of N such that A5: t1 in downarrow J and A6: t <= t1 by A1, A4, YELLOW_4:def_1; consider t2 being Element of N such that A7: t1 <= t2 and A8: t2 in J by A5, WAYBEL_0:def_15; w1 <= t1 by A3, A6, ORDERS_2:3; then w1 <= t2 by A7, ORDERS_2:3; hence w in downarrow J by A8, WAYBEL_0:def_15; ::_thesis: verum end; theorem :: YELLOW12:30 for N being non empty reflexive RelStr for x being Element of N for X being Subset of N st x in X holds uparrow x c= uparrow X proof let N be non empty reflexive RelStr ; ::_thesis: for x being Element of N for X being Subset of N st x in X holds uparrow x c= uparrow X let x be Element of N; ::_thesis: for X being Subset of N st x in X holds uparrow x c= uparrow X let X be Subset of N; ::_thesis: ( x in X implies uparrow x c= uparrow X ) assume A1: x in X ; ::_thesis: uparrow x c= uparrow X let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in uparrow x or a in uparrow X ) assume A2: a in uparrow x ; ::_thesis: a in uparrow X then reconsider b = a as Element of N ; x <= b by A2, WAYBEL_0:18; hence a in uparrow X by A1, WAYBEL_0:def_16; ::_thesis: verum end; theorem :: YELLOW12:31 for N being non empty reflexive RelStr for x being Element of N for X being Subset of N st x in X holds downarrow x c= downarrow X proof let N be non empty reflexive RelStr ; ::_thesis: for x being Element of N for X being Subset of N st x in X holds downarrow x c= downarrow X let x be Element of N; ::_thesis: for X being Subset of N st x in X holds downarrow x c= downarrow X let X be Subset of N; ::_thesis: ( x in X implies downarrow x c= downarrow X ) assume A1: x in X ; ::_thesis: downarrow x c= downarrow X let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in downarrow x or a in downarrow X ) assume A2: a in downarrow x ; ::_thesis: a in downarrow X then reconsider b = a as Element of N ; b <= x by A2, WAYBEL_0:17; hence a in downarrow X by A1, WAYBEL_0:def_15; ::_thesis: verum end; begin theorem Th32: :: YELLOW12:32 for S, T being TopStruct for B being Basis of S st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) holds B is Basis of T proof let S, T be TopStruct ; ::_thesis: for B being Basis of S st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) holds B is Basis of T let B be Basis of S; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) implies B is Basis of T ) A1: B c= the topology of S by TOPS_2:64; assume A2: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: B is Basis of T then the topology of T c= UniCl B by CANTOR_1:def_2; hence B is Basis of T by A2, A1, CANTOR_1:def_2, TOPS_2:64; ::_thesis: verum end; theorem Th33: :: YELLOW12:33 for S, T being TopStruct for B being prebasis of S st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) holds B is prebasis of T proof let S, T be TopStruct ; ::_thesis: for B being prebasis of S st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) holds B is prebasis of T let B be prebasis of S; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) implies B is prebasis of T ) consider F being Basis of S such that A1: F c= FinMeetCl B by CANTOR_1:def_4; assume A2: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: B is prebasis of T then ( B c= the topology of T & F is Basis of T ) by Th32, TOPS_2:64; hence B is prebasis of T by A2, A1, CANTOR_1:def_4, TOPS_2:64; ::_thesis: verum end; theorem Th34: :: YELLOW12:34 for T being non empty TopSpace for J being Basis of T holds not J is empty proof let T be non empty TopSpace; ::_thesis: for J being Basis of T holds not J is empty let J be Basis of T; ::_thesis: not J is empty assume J is empty ; ::_thesis: contradiction then A1: UniCl J = {{}} by YELLOW_9:16; ( the topology of T c= UniCl J & the carrier of T in the topology of T ) by CANTOR_1:def_2, PRE_TOPC:def_1; hence contradiction by A1, TARSKI:def_1; ::_thesis: verum end; registration let T be non empty TopSpace; cluster open quasi_basis -> non empty for Element of bool (bool the carrier of T); coherence for b1 being Basis of T holds not b1 is empty by Th34; end; theorem Th35: :: YELLOW12:35 for T being non empty TopSpace for x being Point of T for J being Basis of x holds not J is empty proof let T be non empty TopSpace; ::_thesis: for x being Point of T for J being Basis of x holds not J is empty let x be Point of T; ::_thesis: for J being Basis of x holds not J is empty let J be Basis of x; ::_thesis: not J is empty ex W being Subset of T st ( W in J & W c= [#] T ) by YELLOW_8:13; hence not J is empty ; ::_thesis: verum end; registration let T be non empty TopSpace; let x be Point of T; cluster open V225(T,x) -> non empty for Element of bool (bool the carrier of T); coherence for b1 being Basis of x holds not b1 is empty by Th35; end; theorem :: YELLOW12:36 for S1, T1, S2, T2 being TopSpace for f being Function of S1,S2 for g being Function of T1,T2 st TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of T1, the topology of T1 #) & TopStruct(# the carrier of S2, the topology of S2 #) = TopStruct(# the carrier of T2, the topology of T2 #) & f = g & f is continuous holds g is continuous proof let S1, T1, S2, T2 be TopSpace; ::_thesis: for f being Function of S1,S2 for g being Function of T1,T2 st TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of T1, the topology of T1 #) & TopStruct(# the carrier of S2, the topology of S2 #) = TopStruct(# the carrier of T2, the topology of T2 #) & f = g & f is continuous holds g is continuous let f be Function of S1,S2; ::_thesis: for g being Function of T1,T2 st TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of T1, the topology of T1 #) & TopStruct(# the carrier of S2, the topology of S2 #) = TopStruct(# the carrier of T2, the topology of T2 #) & f = g & f is continuous holds g is continuous let g be Function of T1,T2; ::_thesis: ( TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of T1, the topology of T1 #) & TopStruct(# the carrier of S2, the topology of S2 #) = TopStruct(# the carrier of T2, the topology of T2 #) & f = g & f is continuous implies g is continuous ) assume that A1: TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of T1, the topology of T1 #) and A2: TopStruct(# the carrier of S2, the topology of S2 #) = TopStruct(# the carrier of T2, the topology of T2 #) and A3: f = g and A4: f is continuous ; ::_thesis: g is continuous now__::_thesis:_for_P2_being_Subset_of_T2_st_P2_is_closed_holds_ g_"_P2_is_closed let P2 be Subset of T2; ::_thesis: ( P2 is closed implies g " P2 is closed ) assume A5: P2 is closed ; ::_thesis: g " P2 is closed reconsider P1 = P2 as Subset of S2 by A2; P1 is closed by A2, A5, TOPS_3:79; then f " P1 is closed by A4, PRE_TOPC:def_6; hence g " P2 is closed by A1, A3, TOPS_3:79; ::_thesis: verum end; hence g is continuous by PRE_TOPC:def_6; ::_thesis: verum end; theorem Th37: :: YELLOW12:37 for T being non empty TopSpace holds id the carrier of T = { p where p is Point of [:T,T:] : (pr1 ( the carrier of T, the carrier of T)) . p = (pr2 ( the carrier of T, the carrier of T)) . p } proof let T be non empty TopSpace; ::_thesis: id the carrier of T = { p where p is Point of [:T,T:] : (pr1 ( the carrier of T, the carrier of T)) . p = (pr2 ( the carrier of T, the carrier of T)) . p } set f = pr1 ( the carrier of T, the carrier of T); set g = pr2 ( the carrier of T, the carrier of T); A1: the carrier of [:T,T:] = [: the carrier of T, the carrier of T:] by BORSUK_1:def_2; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { p where p is Point of [:T,T:] : (pr1 ( the carrier of T, the carrier of T)) . p = (pr2 ( the carrier of T, the carrier of T)) . p } c= id the carrier of T let a be set ; ::_thesis: ( a in id the carrier of T implies a in { p where p is Point of [:T,T:] : (pr1 ( the carrier of T, the carrier of T)) . p = (pr2 ( the carrier of T, the carrier of T)) . p } ) assume A2: a in id the carrier of T ; ::_thesis: a in { p where p is Point of [:T,T:] : (pr1 ( the carrier of T, the carrier of T)) . p = (pr2 ( the carrier of T, the carrier of T)) . p } then consider x, y being set such that A3: x in the carrier of T and A4: y in the carrier of T and A5: a = [x,y] by ZFMISC_1:def_2; A6: x = y by A2, A5, RELAT_1:def_10; (pr1 ( the carrier of T, the carrier of T)) . (x,y) = x by A3, A4, FUNCT_3:def_4 .= (pr2 ( the carrier of T, the carrier of T)) . (x,y) by A3, A6, FUNCT_3:def_5 ; hence a in { p where p is Point of [:T,T:] : (pr1 ( the carrier of T, the carrier of T)) . p = (pr2 ( the carrier of T, the carrier of T)) . p } by A1, A2, A5; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { p where p is Point of [:T,T:] : (pr1 ( the carrier of T, the carrier of T)) . p = (pr2 ( the carrier of T, the carrier of T)) . p } or a in id the carrier of T ) assume a in { p where p is Point of [:T,T:] : (pr1 ( the carrier of T, the carrier of T)) . p = (pr2 ( the carrier of T, the carrier of T)) . p } ; ::_thesis: a in id the carrier of T then consider p being Point of [:T,T:] such that A7: a = p and A8: (pr1 ( the carrier of T, the carrier of T)) . p = (pr2 ( the carrier of T, the carrier of T)) . p ; consider x, y being set such that A9: x in the carrier of T and A10: y in the carrier of T and A11: p = [x,y] by A1, ZFMISC_1:def_2; A12: (pr1 ( the carrier of T, the carrier of T)) . (x,y) = (pr2 ( the carrier of T, the carrier of T)) . (x,y) by A8, A11; x = (pr1 ( the carrier of T, the carrier of T)) . (x,y) by A9, A10, FUNCT_3:def_4 .= y by A9, A10, A12, FUNCT_3:def_5 ; hence a in id the carrier of T by A7, A9, A11, RELAT_1:def_10; ::_thesis: verum end; theorem Th38: :: YELLOW12:38 for T being non empty TopSpace holds delta the carrier of T is continuous Function of T,[:T,T:] proof let T be non empty TopSpace; ::_thesis: delta the carrier of T is continuous Function of T,[:T,T:] the carrier of [:T,T:] = [: the carrier of T, the carrier of T:] by BORSUK_1:def_2; then reconsider f = delta the carrier of T as Function of T,[:T,T:] ; f is continuous proof let W be Point of T; :: according to BORSUK_1:def_1 ::_thesis: for b1 being a_neighborhood of f . W ex b2 being a_neighborhood of W st f .: b2 c= b1 let G be a_neighborhood of f . W; ::_thesis: ex b1 being a_neighborhood of W st f .: b1 c= G consider A being Subset-Family of [:T,T:] such that A1: Int G = union A and A2: for e being set st e in A holds ex X1, Y1 being Subset of T st ( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5; f . W in Int G by CONNSP_2:def_1; then consider Z being set such that A3: f . W in Z and A4: Z in A by A1, TARSKI:def_4; consider X1, Y1 being Subset of T such that A5: Z = [:X1,Y1:] and A6: ( X1 is open & Y1 is open ) by A2, A4; f . W = [W,W] by FUNCT_3:def_6; then ( W in X1 & W in Y1 ) by A3, A5, ZFMISC_1:87; then A7: W in X1 /\ Y1 by XBOOLE_0:def_4; X1 /\ Y1 is open by A6; then W in Int (X1 /\ Y1) by A7, TOPS_1:23; then reconsider H = X1 /\ Y1 as a_neighborhood of W by CONNSP_2:def_1; A8: f .: H c= Int G proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: H or y in Int G ) assume y in f .: H ; ::_thesis: y in Int G then consider x being set such that A9: x in dom f and A10: x in H and A11: y = f . x by FUNCT_1:def_6; A12: ( x in X1 & x in Y1 ) by A10, XBOOLE_0:def_4; y = [x,x] by A9, A11, FUNCT_3:def_6; then y in Z by A5, A12, ZFMISC_1:87; hence y in Int G by A1, A4, TARSKI:def_4; ::_thesis: verum end; take H ; ::_thesis: f .: H c= G Int G c= G by TOPS_1:16; hence f .: H c= G by A8, XBOOLE_1:1; ::_thesis: verum end; hence delta the carrier of T is continuous Function of T,[:T,T:] ; ::_thesis: verum end; theorem Th39: :: YELLOW12:39 for S, T being non empty TopSpace holds pr1 ( the carrier of S, the carrier of T) is continuous Function of [:S,T:],S proof let S, T be non empty TopSpace; ::_thesis: pr1 ( the carrier of S, the carrier of T) is continuous Function of [:S,T:],S set I = the carrier of S; set J = the carrier of T; A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by BORSUK_1:def_2; then reconsider f = pr1 ( the carrier of S, the carrier of T) as Function of [:S,T:],S ; f is continuous proof let w be Point of [:S,T:]; :: according to BORSUK_1:def_1 ::_thesis: for b1 being a_neighborhood of f . w ex b2 being a_neighborhood of w st f .: b2 c= b1 let G be a_neighborhood of f . w; ::_thesis: ex b1 being a_neighborhood of w st f .: b1 c= G set H = [:(Int G),([#] T):]; A2: Int [:(Int G),([#] T):] = [:(Int (Int G)),(Int ([#] T)):] by BORSUK_1:7 .= [:(Int G),([#] T):] by TOPS_1:15 ; consider x, y being set such that A3: x in the carrier of S and A4: y in the carrier of T and A5: w = [x,y] by A1, ZFMISC_1:def_2; ( f . w in Int G & f . (x,y) = x ) by A3, A4, CONNSP_2:def_1, FUNCT_3:def_4; then w in Int [:(Int G),([#] T):] by A4, A5, A2, ZFMISC_1:def_2; then reconsider H = [:(Int G),([#] T):] as a_neighborhood of w by CONNSP_2:def_1; take H ; ::_thesis: f .: H c= G reconsider X = Int G as non empty Subset of S by CONNSP_2:def_1; [:X,([#] T):] <> {} ; then f .: H = Int G by EQREL_1:49; hence f .: H c= G by TOPS_1:16; ::_thesis: verum end; hence pr1 ( the carrier of S, the carrier of T) is continuous Function of [:S,T:],S ; ::_thesis: verum end; theorem Th40: :: YELLOW12:40 for S, T being non empty TopSpace holds pr2 ( the carrier of S, the carrier of T) is continuous Function of [:S,T:],T proof let S, T be non empty TopSpace; ::_thesis: pr2 ( the carrier of S, the carrier of T) is continuous Function of [:S,T:],T set I = the carrier of S; set J = the carrier of T; A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by BORSUK_1:def_2; then reconsider f = pr2 ( the carrier of S, the carrier of T) as Function of [:S,T:],T ; f is continuous proof let w be Point of [:S,T:]; :: according to BORSUK_1:def_1 ::_thesis: for b1 being a_neighborhood of f . w ex b2 being a_neighborhood of w st f .: b2 c= b1 let G be a_neighborhood of f . w; ::_thesis: ex b1 being a_neighborhood of w st f .: b1 c= G set H = [:([#] S),(Int G):]; A2: Int [:([#] S),(Int G):] = [:(Int ([#] S)),(Int (Int G)):] by BORSUK_1:7 .= [:([#] S),(Int G):] by TOPS_1:15 ; consider x, y being set such that A3: x in the carrier of S and A4: y in the carrier of T and A5: w = [x,y] by A1, ZFMISC_1:def_2; ( f . w in Int G & f . (x,y) = y ) by A3, A4, CONNSP_2:def_1, FUNCT_3:def_5; then w in Int [:([#] S),(Int G):] by A3, A5, A2, ZFMISC_1:def_2; then reconsider H = [:([#] S),(Int G):] as a_neighborhood of w by CONNSP_2:def_1; take H ; ::_thesis: f .: H c= G reconsider X = Int G as non empty Subset of T by CONNSP_2:def_1; [:([#] S),X:] <> {} ; then f .: H = Int G by EQREL_1:49; hence f .: H c= G by TOPS_1:16; ::_thesis: verum end; hence pr2 ( the carrier of S, the carrier of T) is continuous Function of [:S,T:],T ; ::_thesis: verum end; theorem Th41: :: YELLOW12:41 for T, S, R being non empty TopSpace for f being continuous Function of T,S for g being continuous Function of T,R holds <:f,g:> is continuous Function of T,[:S,R:] proof let T, S, R be non empty TopSpace; ::_thesis: for f being continuous Function of T,S for g being continuous Function of T,R holds <:f,g:> is continuous Function of T,[:S,R:] let f be continuous Function of T,S; ::_thesis: for g being continuous Function of T,R holds <:f,g:> is continuous Function of T,[:S,R:] let g be continuous Function of T,R; ::_thesis: <:f,g:> is continuous Function of T,[:S,R:] A1: <:f,g:> = [:f,g:] * (delta the carrier of T) by FUNCT_3:78; delta the carrier of T is continuous Function of T,[:T,T:] by Th38; hence <:f,g:> is continuous Function of T,[:S,R:] by A1; ::_thesis: verum end; theorem Th42: :: YELLOW12:42 for S, T being non empty TopSpace holds <:(pr2 ( the carrier of S, the carrier of T)),(pr1 ( the carrier of S, the carrier of T)):> is continuous Function of [:S,T:],[:T,S:] proof let S, T be non empty TopSpace; ::_thesis: <:(pr2 ( the carrier of S, the carrier of T)),(pr1 ( the carrier of S, the carrier of T)):> is continuous Function of [:S,T:],[:T,S:] ( pr1 ( the carrier of S, the carrier of T) is continuous Function of [:S,T:],S & pr2 ( the carrier of S, the carrier of T) is continuous Function of [:S,T:],T ) by Th39, Th40; hence <:(pr2 ( the carrier of S, the carrier of T)),(pr1 ( the carrier of S, the carrier of T)):> is continuous Function of [:S,T:],[:T,S:] by Th41; ::_thesis: verum end; theorem Th43: :: YELLOW12:43 for S, T being non empty TopSpace for f being Function of [:S,T:],[:T,S:] st f = <:(pr2 ( the carrier of S, the carrier of T)),(pr1 ( the carrier of S, the carrier of T)):> holds f is being_homeomorphism proof let S, T be non empty TopSpace; ::_thesis: for f being Function of [:S,T:],[:T,S:] st f = <:(pr2 ( the carrier of S, the carrier of T)),(pr1 ( the carrier of S, the carrier of T)):> holds f is being_homeomorphism let f be Function of [:S,T:],[:T,S:]; ::_thesis: ( f = <:(pr2 ( the carrier of S, the carrier of T)),(pr1 ( the carrier of S, the carrier of T)):> implies f is being_homeomorphism ) assume A1: f = <:(pr2 ( the carrier of S, the carrier of T)),(pr1 ( the carrier of S, the carrier of T)):> ; ::_thesis: f is being_homeomorphism thus dom f = [#] [:S,T:] by FUNCT_2:def_1; :: according to TOPS_2:def_5 ::_thesis: ( rng f = [#] [:T,S:] & f is one-to-one & f is continuous & f " is continuous ) thus A2: rng f = [: the carrier of T, the carrier of S:] by A1, Th4 .= [#] [:T,S:] by BORSUK_1:def_2 ; ::_thesis: ( f is one-to-one & f is continuous & f " is continuous ) thus f is one-to-one by A1; ::_thesis: ( f is continuous & f " is continuous ) thus f is continuous by A1, Th42; ::_thesis: f " is continuous f is onto by A2, FUNCT_2:def_3; then f " = f " by A1, TOPS_2:def_4 .= <:(pr2 ( the carrier of T, the carrier of S)),(pr1 ( the carrier of T, the carrier of S)):> by A1, Th8 ; hence f " is continuous by Th42; ::_thesis: verum end; theorem :: YELLOW12:44 for S, T being non empty TopSpace holds [:S,T:],[:T,S:] are_homeomorphic proof let S, T be non empty TopSpace; ::_thesis: [:S,T:],[:T,S:] are_homeomorphic reconsider f = <:(pr2 ( the carrier of S, the carrier of T)),(pr1 ( the carrier of S, the carrier of T)):> as Function of [:S,T:],[:T,S:] by Th42; take f ; :: according to T_0TOPSP:def_1 ::_thesis: f is being_homeomorphism thus f is being_homeomorphism by Th43; ::_thesis: verum end; theorem Th45: :: YELLOW12:45 for S being non empty TopSpace for T being non empty Hausdorff TopSpace for f, g being continuous Function of S,T holds ( ( for X being Subset of S st X = { p where p is Point of S : f . p <> g . p } holds X is open ) & ( for X being Subset of S st X = { p where p is Point of S : f . p = g . p } holds X is closed ) ) proof let S be non empty TopSpace; ::_thesis: for T being non empty Hausdorff TopSpace for f, g being continuous Function of S,T holds ( ( for X being Subset of S st X = { p where p is Point of S : f . p <> g . p } holds X is open ) & ( for X being Subset of S st X = { p where p is Point of S : f . p = g . p } holds X is closed ) ) let T be non empty Hausdorff TopSpace; ::_thesis: for f, g being continuous Function of S,T holds ( ( for X being Subset of S st X = { p where p is Point of S : f . p <> g . p } holds X is open ) & ( for X being Subset of S st X = { p where p is Point of S : f . p = g . p } holds X is closed ) ) let f, g be continuous Function of S,T; ::_thesis: ( ( for X being Subset of S st X = { p where p is Point of S : f . p <> g . p } holds X is open ) & ( for X being Subset of S st X = { p where p is Point of S : f . p = g . p } holds X is closed ) ) { p where p is Point of S : f . p <> g . p } c= the carrier of S proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Point of S : f . p <> g . p } or x in the carrier of S ) assume x in { p where p is Point of S : f . p <> g . p } ; ::_thesis: x in the carrier of S then ex a being Point of S st ( x = a & f . a <> g . a ) ; hence x in the carrier of S ; ::_thesis: verum end; then reconsider A = { p where p is Point of S : f . p <> g . p } as Subset of S ; A1: [#] T <> {} ; thus for X being Subset of S st X = { p where p is Point of S : f . p <> g . p } holds X is open ::_thesis: for X being Subset of S st X = { p where p is Point of S : f . p = g . p } holds X is closed proof let X be Subset of S; ::_thesis: ( X = { p where p is Point of S : f . p <> g . p } implies X is open ) assume A2: X = { p where p is Point of S : f . p <> g . p } ; ::_thesis: X is open for x being set holds ( x in X iff ex Q being Subset of S st ( Q is open & Q c= X & x in Q ) ) proof let x be set ; ::_thesis: ( x in X iff ex Q being Subset of S st ( Q is open & Q c= X & x in Q ) ) hereby ::_thesis: ( ex Q being Subset of S st ( Q is open & Q c= X & x in Q ) implies x in X ) assume x in X ; ::_thesis: ex Q being Element of bool the carrier of S st ( Q is open & Q c= X & x in Q ) then consider p being Point of S such that A3: x = p and A4: f . p <> g . p by A2; consider W, V being Subset of T such that A5: ( W is open & V is open ) and A6: f . p in W and A7: g . p in V and A8: W misses V by A4, PRE_TOPC:def_10; dom g = the carrier of S by FUNCT_2:def_1; then [x,(g . p)] in g by A3, FUNCT_1:def_2; then A9: x in g " V by A7, RELAT_1:def_14; take Q = (f " W) /\ (g " V); ::_thesis: ( Q is open & Q c= X & x in Q ) ( f " W is open & g " V is open ) by A1, A5, TOPS_2:43; hence Q is open ; ::_thesis: ( Q c= X & x in Q ) thus Q c= X ::_thesis: x in Q proof let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in Q or q in X ) assume A10: q in Q ; ::_thesis: q in X then q in f " W by XBOOLE_0:def_4; then consider yf being set such that A11: [q,yf] in f and A12: yf in W by RELAT_1:def_14; q in g " V by A10, XBOOLE_0:def_4; then consider yg being set such that A13: ( [q,yg] in g & yg in V ) by RELAT_1:def_14; A14: ( yg = g . q & not yg in W ) by A8, A13, FUNCT_1:1, XBOOLE_0:3; yf = f . q by A11, FUNCT_1:1; hence q in X by A2, A10, A12, A14; ::_thesis: verum end; dom f = the carrier of S by FUNCT_2:def_1; then [x,(f . p)] in f by A3, FUNCT_1:def_2; then x in f " W by A6, RELAT_1:def_14; hence x in Q by A9, XBOOLE_0:def_4; ::_thesis: verum end; given Q being Subset of S such that Q is open and A15: ( Q c= X & x in Q ) ; ::_thesis: x in X thus x in X by A15; ::_thesis: verum end; hence X is open by TOPS_1:25; ::_thesis: verum end; then A16: A is open ; let X be Subset of S; ::_thesis: ( X = { p where p is Point of S : f . p = g . p } implies X is closed ) assume A17: X = { p where p is Point of S : f . p = g . p } ; ::_thesis: X is closed X ` = A proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: A c= X ` let x be set ; ::_thesis: ( x in X ` implies x in A ) assume A18: x in X ` ; ::_thesis: x in A then not x in X by XBOOLE_0:def_5; then f . x <> g . x by A17, A18; hence x in A by A18; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in X ` ) assume x in A ; ::_thesis: x in X ` then consider p being Point of S such that A19: x = p and A20: f . p <> g . p ; now__::_thesis:_not_p_in__{__t_where_t_is_Point_of_S_:_f_._t_=_g_._t__}_ assume p in { t where t is Point of S : f . t = g . t } ; ::_thesis: contradiction then ex t being Point of S st ( p = t & f . t = g . t ) ; hence contradiction by A20; ::_thesis: verum end; hence x in X ` by A17, A19, XBOOLE_0:def_5; ::_thesis: verum end; hence X is closed by A16, TOPS_1:3; ::_thesis: verum end; theorem :: YELLOW12:46 for T being non empty TopSpace holds ( T is Hausdorff iff for A being Subset of [:T,T:] st A = id the carrier of T holds A is closed ) proof let T be non empty TopSpace; ::_thesis: ( T is Hausdorff iff for A being Subset of [:T,T:] st A = id the carrier of T holds A is closed ) reconsider f = pr1 ( the carrier of T, the carrier of T), g = pr2 ( the carrier of T, the carrier of T) as continuous Function of [:T,T:],T by Th39, Th40; reconsider A = id the carrier of T as Subset of [:T,T:] by BORSUK_1:def_2; hereby ::_thesis: ( ( for A being Subset of [:T,T:] st A = id the carrier of T holds A is closed ) implies T is Hausdorff ) assume A1: T is Hausdorff ; ::_thesis: for A being Subset of [:T,T:] st A = id the carrier of T holds A is closed let A be Subset of [:T,T:]; ::_thesis: ( A = id the carrier of T implies A is closed ) assume A = id the carrier of T ; ::_thesis: A is closed then A = { p where p is Point of [:T,T:] : f . p = g . p } by Th37; hence A is closed by A1, Th45; ::_thesis: verum end; assume for A being Subset of [:T,T:] st A = id the carrier of T holds A is closed ; ::_thesis: T is Hausdorff then ( [#] [:T,T:] = [:([#] T),([#] T):] & A is closed ) by BORSUK_1:def_2; then [:([#] T),([#] T):] \ A is open by PRE_TOPC:def_3; then consider SF being Subset-Family of [:T,T:] such that A2: [:([#] T),([#] T):] \ A = union SF and A3: for e being set st e in SF holds ex X1, Y1 being Subset of T st ( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5; let p, q be Point of T; :: according to PRE_TOPC:def_10 ::_thesis: ( p = q or ex b1, b2 being Element of bool the carrier of T st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) ) assume not p = q ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) then ( the carrier of [:T,T:] = [: the carrier of T, the carrier of T:] & not [p,q] in id ([#] T) ) by BORSUK_1:def_2, RELAT_1:def_10; then [p,q] in [:([#] T),([#] T):] \ A by XBOOLE_0:def_5; then consider XY being set such that A4: [p,q] in XY and A5: XY in SF by A2, TARSKI:def_4; consider X1, Y1 being Subset of T such that A6: XY = [:X1,Y1:] and A7: ( X1 is open & Y1 is open ) by A3, A5; take X1 ; ::_thesis: ex b1 being Element of bool the carrier of T st ( X1 is open & b1 is open & p in X1 & q in b1 & X1 misses b1 ) take Y1 ; ::_thesis: ( X1 is open & Y1 is open & p in X1 & q in Y1 & X1 misses Y1 ) thus ( X1 is open & Y1 is open ) by A7; ::_thesis: ( p in X1 & q in Y1 & X1 misses Y1 ) thus ( p in X1 & q in Y1 ) by A4, A6, ZFMISC_1:87; ::_thesis: X1 misses Y1 assume X1 /\ Y1 <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then consider w being set such that A8: w in X1 /\ Y1 by XBOOLE_0:def_1; ( w in X1 & w in Y1 ) by A8, XBOOLE_0:def_4; then [w,w] in XY by A6, ZFMISC_1:87; then [w,w] in union SF by A5, TARSKI:def_4; then not [w,w] in A by A2, XBOOLE_0:def_5; hence contradiction by A8, RELAT_1:def_10; ::_thesis: verum end; registration let S, T be TopStruct ; cluster strict TopSpace-like for Refinement of S,T; existence ex b1 being Refinement of S,T st b1 is strict proof set R = the Refinement of S,T; set R1 = TopStruct(# the carrier of the Refinement of S,T, the topology of the Refinement of S,T #); the topology of S \/ the topology of T is prebasis of the Refinement of S,T by YELLOW_9:def_6; then ( the carrier of TopStruct(# the carrier of the Refinement of S,T, the topology of the Refinement of S,T #) = the carrier of S \/ the carrier of T & the topology of S \/ the topology of T is prebasis of TopStruct(# the carrier of the Refinement of S,T, the topology of the Refinement of S,T #) ) by Th33, YELLOW_9:def_6; then reconsider R1 = TopStruct(# the carrier of the Refinement of S,T, the topology of the Refinement of S,T #) as Refinement of S,T by YELLOW_9:def_6; take R1 ; ::_thesis: R1 is strict thus R1 is strict ; ::_thesis: verum end; end; registration let S be non empty TopStruct ; let T be TopStruct ; cluster non empty strict TopSpace-like for Refinement of S,T; existence ex b1 being Refinement of S,T st ( b1 is strict & not b1 is empty ) proof set R = the strict Refinement of S,T; take the strict Refinement of S,T ; ::_thesis: ( the strict Refinement of S,T is strict & not the strict Refinement of S,T is empty ) thus ( the strict Refinement of S,T is strict & not the strict Refinement of S,T is empty ) ; ::_thesis: verum end; cluster non empty strict TopSpace-like for Refinement of T,S; existence ex b1 being Refinement of T,S st ( b1 is strict & not b1 is empty ) proof set R = the strict Refinement of T,S; take the strict Refinement of T,S ; ::_thesis: ( the strict Refinement of T,S is strict & not the strict Refinement of T,S is empty ) thus ( the strict Refinement of T,S is strict & not the strict Refinement of T,S is empty ) ; ::_thesis: verum end; end; theorem :: YELLOW12:47 for R, S, T being TopStruct holds ( R is Refinement of S,T iff TopStruct(# the carrier of R, the topology of R #) is Refinement of S,T ) proof let R, S, T be TopStruct ; ::_thesis: ( R is Refinement of S,T iff TopStruct(# the carrier of R, the topology of R #) is Refinement of S,T ) hereby ::_thesis: ( TopStruct(# the carrier of R, the topology of R #) is Refinement of S,T implies R is Refinement of S,T ) assume A1: R is Refinement of S,T ; ::_thesis: TopStruct(# the carrier of R, the topology of R #) is Refinement of S,T then reconsider R1 = R as TopSpace ; the topology of S \/ the topology of T is prebasis of R by A1, YELLOW_9:def_6; then A2: the topology of S \/ the topology of T is prebasis of TopStruct(# the carrier of R1, the topology of R1 #) by Th33; the carrier of TopStruct(# the carrier of R1, the topology of R1 #) = the carrier of S \/ the carrier of T by A1, YELLOW_9:def_6; hence TopStruct(# the carrier of R, the topology of R #) is Refinement of S,T by A2, YELLOW_9:def_6; ::_thesis: verum end; assume A3: TopStruct(# the carrier of R, the topology of R #) is Refinement of S,T ; ::_thesis: R is Refinement of S,T then reconsider R1 = R as TopSpace by TEX_2:7; the topology of S \/ the topology of T is prebasis of TopStruct(# the carrier of R, the topology of R #) by A3, YELLOW_9:def_6; then A4: the topology of S \/ the topology of T is prebasis of R1 by Th33; the carrier of R1 = the carrier of S \/ the carrier of T by A3, YELLOW_9:def_6; hence R is Refinement of S,T by A4, YELLOW_9:def_6; ::_thesis: verum end; theorem Th48: :: YELLOW12:48 for S1, S2, T1, T2 being non empty TopSpace for R being Refinement of [:S1,T1:],[:S2,T2:] st the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 holds { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } is Basis of R proof let S1, S2, T1, T2 be non empty TopSpace; ::_thesis: for R being Refinement of [:S1,T1:],[:S2,T2:] st the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 holds { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } is Basis of R let R be Refinement of [:S1,T1:],[:S2,T2:]; ::_thesis: ( the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 implies { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } is Basis of R ) assume A1: ( the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 ) ; ::_thesis: { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } is Basis of R set Y = { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } ; A2: the carrier of [:S2,T2:] = [: the carrier of S2, the carrier of T2:] by BORSUK_1:def_2; A3: the carrier of [:S1,T1:] = [: the carrier of S1, the carrier of T1:] by BORSUK_1:def_2; then reconsider BST = INTERSECTION ( the topology of [:S1,T1:], the topology of [:S2,T2:]) as Basis of R by A1, A2, YELLOW_9:60; A4: the carrier of R = the carrier of [:S1,T1:] \/ the carrier of [:S2,T2:] by YELLOW_9:def_6 .= [: the carrier of S1, the carrier of T1:] \/ [: the carrier of S2, the carrier of T2:] by A3, BORSUK_1:def_2 .= [: the carrier of S1, the carrier of T1:] by A1 ; { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } c= bool the carrier of R proof let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } or c in bool the carrier of R ) assume c in { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } ; ::_thesis: c in bool the carrier of R then ex U1 being Subset of S1 ex U2 being Subset of S2 ex V1 being Subset of T1 ex V2 being Subset of T2 st ( c = [:U1,V1:] /\ [:U2,V2:] & U1 is open & U2 is open & V1 is open & V2 is open ) ; hence c in bool the carrier of R by A1, A2, A4; ::_thesis: verum end; then reconsider C1 = { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } as Subset-Family of R ; reconsider C1 = C1 as Subset-Family of R ; A5: the topology of [:S2,T2:] = { (union A) where A is Subset-Family of [:S2,T2:] : A c= { [:X1,Y1:] where X1 is Subset of S2, Y1 is Subset of T2 : ( X1 in the topology of S2 & Y1 in the topology of T2 ) } } by BORSUK_1:def_2; A6: the topology of [:S1,T1:] = { (union A) where A is Subset-Family of [:S1,T1:] : A c= { [:X1,Y1:] where X1 is Subset of S1, Y1 is Subset of T1 : ( X1 in the topology of S1 & Y1 in the topology of T1 ) } } by BORSUK_1:def_2; A7: for A being Subset of R st A is open holds for p being Point of R st p in A holds ex a being Subset of R st ( a in C1 & p in a & a c= A ) proof let A be Subset of R; ::_thesis: ( A is open implies for p being Point of R st p in A holds ex a being Subset of R st ( a in C1 & p in a & a c= A ) ) assume A8: A is open ; ::_thesis: for p being Point of R st p in A holds ex a being Subset of R st ( a in C1 & p in a & a c= A ) let p be Point of R; ::_thesis: ( p in A implies ex a being Subset of R st ( a in C1 & p in a & a c= A ) ) assume p in A ; ::_thesis: ex a being Subset of R st ( a in C1 & p in a & a c= A ) then consider X being Subset of R such that A9: X in BST and A10: p in X and A11: X c= A by A8, YELLOW_9:31; consider X1, X2 being set such that A12: X1 in the topology of [:S1,T1:] and A13: X2 in the topology of [:S2,T2:] and A14: X = X1 /\ X2 by A9, SETFAM_1:def_5; consider F1 being Subset-Family of [:S1,T1:] such that A15: X1 = union F1 and A16: F1 c= { [:K1,L1:] where K1 is Subset of S1, L1 is Subset of T1 : ( K1 in the topology of S1 & L1 in the topology of T1 ) } by A6, A12; p in X1 by A10, A14, XBOOLE_0:def_4; then consider G1 being set such that A17: p in G1 and A18: G1 in F1 by A15, TARSKI:def_4; A19: G1 in { [:K1,L1:] where K1 is Subset of S1, L1 is Subset of T1 : ( K1 in the topology of S1 & L1 in the topology of T1 ) } by A16, A18; consider F2 being Subset-Family of [:S2,T2:] such that A20: X2 = union F2 and A21: F2 c= { [:K2,L2:] where K2 is Subset of S2, L2 is Subset of T2 : ( K2 in the topology of S2 & L2 in the topology of T2 ) } by A5, A13; p in X2 by A10, A14, XBOOLE_0:def_4; then consider G2 being set such that A22: p in G2 and A23: G2 in F2 by A20, TARSKI:def_4; G2 in { [:K2,L2:] where K2 is Subset of S2, L2 is Subset of T2 : ( K2 in the topology of S2 & L2 in the topology of T2 ) } by A21, A23; then consider K2 being Subset of S2, L2 being Subset of T2 such that A24: G2 = [:K2,L2:] and A25: ( K2 in the topology of S2 & L2 in the topology of T2 ) ; A26: [:K2,L2:] c= X2 by A20, A23, A24, ZFMISC_1:74; A27: ( K2 is open & L2 is open ) by A25, PRE_TOPC:def_2; consider K1 being Subset of S1, L1 being Subset of T1 such that A28: G1 = [:K1,L1:] and A29: ( K1 in the topology of S1 & L1 in the topology of T1 ) by A19; reconsider a = [:K1,L1:] /\ [:K2,L2:] as Subset of R by A1, A4, BORSUK_1:def_2; take a ; ::_thesis: ( a in C1 & p in a & a c= A ) ( K1 is open & L1 is open ) by A29, PRE_TOPC:def_2; hence a in C1 by A27; ::_thesis: ( p in a & a c= A ) thus p in a by A17, A22, A28, A24, XBOOLE_0:def_4; ::_thesis: a c= A [:K1,L1:] c= X1 by A15, A18, A28, ZFMISC_1:74; then a c= X by A14, A26, XBOOLE_1:27; hence a c= A by A11, XBOOLE_1:1; ::_thesis: verum end; { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } c= the topology of R proof let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } or c in the topology of R ) A30: BST c= the topology of R by TOPS_2:64; assume c in { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } ; ::_thesis: c in the topology of R then consider U1 being Subset of S1, U2 being Subset of S2, V1 being Subset of T1, V2 being Subset of T2 such that A31: c = [:U1,V1:] /\ [:U2,V2:] and A32: U1 is open and A33: U2 is open and A34: V1 is open and A35: V2 is open ; [:U2,V2:] is open by A33, A35, BORSUK_1:6; then A36: [:U2,V2:] in the topology of [:S2,T2:] by PRE_TOPC:def_2; [:U1,V1:] is open by A32, A34, BORSUK_1:6; then [:U1,V1:] in the topology of [:S1,T1:] by PRE_TOPC:def_2; then c in BST by A31, A36, SETFAM_1:def_5; hence c in the topology of R by A30; ::_thesis: verum end; hence { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } is Basis of R by A7, YELLOW_9:32; ::_thesis: verum end; theorem Th49: :: YELLOW12:49 for S1, S2, T1, T2 being non empty TopSpace for R being Refinement of [:S1,T1:],[:S2,T2:] for R1 being Refinement of S1,S2 for R2 being Refinement of T1,T2 st the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 holds ( the carrier of [:R1,R2:] = the carrier of R & the topology of [:R1,R2:] = the topology of R ) proof let S1, S2, T1, T2 be non empty TopSpace; ::_thesis: for R being Refinement of [:S1,T1:],[:S2,T2:] for R1 being Refinement of S1,S2 for R2 being Refinement of T1,T2 st the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 holds ( the carrier of [:R1,R2:] = the carrier of R & the topology of [:R1,R2:] = the topology of R ) let R be Refinement of [:S1,T1:],[:S2,T2:]; ::_thesis: for R1 being Refinement of S1,S2 for R2 being Refinement of T1,T2 st the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 holds ( the carrier of [:R1,R2:] = the carrier of R & the topology of [:R1,R2:] = the topology of R ) let R1 be Refinement of S1,S2; ::_thesis: for R2 being Refinement of T1,T2 st the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 holds ( the carrier of [:R1,R2:] = the carrier of R & the topology of [:R1,R2:] = the topology of R ) let R2 be Refinement of T1,T2; ::_thesis: ( the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 implies ( the carrier of [:R1,R2:] = the carrier of R & the topology of [:R1,R2:] = the topology of R ) ) assume that A1: the carrier of S1 = the carrier of S2 and A2: the carrier of T1 = the carrier of T2 ; ::_thesis: ( the carrier of [:R1,R2:] = the carrier of R & the topology of [:R1,R2:] = the topology of R ) A3: the carrier of R1 = the carrier of S1 \/ the carrier of S2 by YELLOW_9:def_6 .= the carrier of S1 by A1 ; set C = { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } ; reconsider BT = INTERSECTION ( the topology of T1, the topology of T2) as Basis of R2 by A2, YELLOW_9:60; reconsider BS = INTERSECTION ( the topology of S1, the topology of S2) as Basis of R1 by A1, YELLOW_9:60; reconsider Bpr = { [:a,b:] where a is Subset of R1, b is Subset of R2 : ( a in BS & b in BT ) } as Basis of [:R1,R2:] by YELLOW_9:40; A4: { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } = Bpr proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: Bpr c= { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } let c be set ; ::_thesis: ( c in { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } implies c in Bpr ) assume c in { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } ; ::_thesis: c in Bpr then consider U1 being Subset of S1, U2 being Subset of S2, V1 being Subset of T1, V2 being Subset of T2 such that A5: c = [:U1,V1:] /\ [:U2,V2:] and A6: ( U1 is open & U2 is open ) and A7: ( V1 is open & V2 is open ) ; ( U1 in the topology of S1 & U2 in the topology of S2 ) by A6, PRE_TOPC:def_2; then A8: U1 /\ U2 in BS by SETFAM_1:def_5; ( V1 in the topology of T1 & V2 in the topology of T2 ) by A7, PRE_TOPC:def_2; then A9: V1 /\ V2 in BT by SETFAM_1:def_5; c = [:(U1 /\ U2),(V1 /\ V2):] by A5, ZFMISC_1:100; hence c in Bpr by A8, A9; ::_thesis: verum end; let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in Bpr or c in { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } ) assume c in Bpr ; ::_thesis: c in { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } then consider a being Subset of R1, b being Subset of R2 such that A10: c = [:a,b:] and A11: a in BS and A12: b in BT ; consider a1, a2 being set such that A13: a1 in the topology of S1 and A14: a2 in the topology of S2 and A15: a = a1 /\ a2 by A11, SETFAM_1:def_5; reconsider a2 = a2 as Subset of S2 by A14; reconsider a1 = a1 as Subset of S1 by A13; A16: ( a1 is open & a2 is open ) by A13, A14, PRE_TOPC:def_2; consider b1, b2 being set such that A17: b1 in the topology of T1 and A18: b2 in the topology of T2 and A19: b = b1 /\ b2 by A12, SETFAM_1:def_5; reconsider b2 = b2 as Subset of T2 by A18; reconsider b1 = b1 as Subset of T1 by A17; A20: ( b1 is open & b2 is open ) by A17, A18, PRE_TOPC:def_2; c = [:a1,b1:] /\ [:a2,b2:] by A10, A15, A19, ZFMISC_1:100; hence c in { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } by A16, A20; ::_thesis: verum end; A21: the carrier of R2 = the carrier of T1 \/ the carrier of T2 by YELLOW_9:def_6 .= the carrier of T1 by A2 ; A22: the carrier of [:S1,T1:] = [: the carrier of S1, the carrier of T1:] by BORSUK_1:def_2; the carrier of R = the carrier of [:S1,T1:] \/ the carrier of [:S2,T2:] by YELLOW_9:def_6 .= [: the carrier of S1, the carrier of T1:] \/ [: the carrier of S2, the carrier of T2:] by A22, BORSUK_1:def_2 .= [: the carrier of S1, the carrier of T1:] by A1, A2 ; hence A23: the carrier of [:R1,R2:] = the carrier of R by A3, A21, BORSUK_1:def_2; ::_thesis: the topology of [:R1,R2:] = the topology of R { ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } is Basis of R by A1, A2, Th48; hence the topology of [:R1,R2:] = the topology of R by A23, A4, YELLOW_9:25; ::_thesis: verum end; theorem :: YELLOW12:50 for S1, S2, T1, T2 being non empty TopSpace for R1 being Refinement of S1,S2 for R2 being Refinement of T1,T2 st the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 holds [:R1,R2:] is Refinement of [:S1,T1:],[:S2,T2:] proof let S1, S2, T1, T2 be non empty TopSpace; ::_thesis: for R1 being Refinement of S1,S2 for R2 being Refinement of T1,T2 st the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 holds [:R1,R2:] is Refinement of [:S1,T1:],[:S2,T2:] let R1 be Refinement of S1,S2; ::_thesis: for R2 being Refinement of T1,T2 st the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 holds [:R1,R2:] is Refinement of [:S1,T1:],[:S2,T2:] let R2 be Refinement of T1,T2; ::_thesis: ( the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 implies [:R1,R2:] is Refinement of [:S1,T1:],[:S2,T2:] ) set R = the strict Refinement of [:S1,T1:],[:S2,T2:]; assume A1: ( the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 ) ; ::_thesis: [:R1,R2:] is Refinement of [:S1,T1:],[:S2,T2:] then the carrier of [:R1,R2:] = the carrier of the strict Refinement of [:S1,T1:],[:S2,T2:] by Th49; hence [:R1,R2:] is Refinement of [:S1,T1:],[:S2,T2:] by A1, Th49; ::_thesis: verum end;