:: 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;