let X, Z be non empty TopSpace; :: thesis: for Y being non empty SubSpace of Z holds oContMaps (X,Y) is full SubRelStr of oContMaps (X,Z)
let Y be non empty SubSpace of Z; :: thesis: oContMaps (X,Y) is full SubRelStr of oContMaps (X,Z)
set XY = oContMaps (X,Y);
set XZ = oContMaps (X,Z);
A1: Omega Y is full SubRelStr of Omega Z by WAYBEL25:17;
A2: [#] Y c= [#] Z by PRE_TOPC:def 4;
oContMaps (X,Y) is SubRelStr of oContMaps (X,Z)
proof
thus A3: the carrier of (oContMaps (X,Y)) c= the carrier of (oContMaps (X,Z)) :: according to YELLOW_0:def 13 :: thesis: the InternalRel of (oContMaps (X,Y)) c= the InternalRel of (oContMaps (X,Z))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (oContMaps (X,Y)) or x in the carrier of (oContMaps (X,Z)) )
assume x in the carrier of (oContMaps (X,Y)) ; :: thesis: x in the carrier of (oContMaps (X,Z))
then reconsider f = x as continuous Function of X,Y by Th2;
( dom f = the carrier of X & rng f c= the carrier of Z ) by ;
then x is continuous Function of X,Z by ;
then x is Element of (oContMaps (X,Z)) by Th2;
hence x in the carrier of (oContMaps (X,Z)) ; :: thesis: verum
end;
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in the InternalRel of (oContMaps (X,Y)) or [x,y] in the InternalRel of (oContMaps (X,Z)) )
assume A4: [x,y] in the InternalRel of (oContMaps (X,Y)) ; :: thesis: [x,y] in the InternalRel of (oContMaps (X,Z))
reconsider x = x, y = y as Element of (oContMaps (X,Y)) by ;
reconsider a = x, b = y as Element of (oContMaps (X,Z)) by A3;
reconsider f = x, g = y as continuous Function of X,() by Th1;
reconsider f9 = a, g9 = b as continuous Function of X,() by Th1;
x <= y by ;
then f <= g by Th3;
then f9 <= g9 by ;
then a <= b by Th3;
hence [x,y] in the InternalRel of (oContMaps (X,Z)) by ORDERS_2:def 5; :: thesis: verum
end;
then reconsider XY = oContMaps (X,Y) as non empty SubRelStr of oContMaps (X,Z) ;
A5: the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY = the InternalRel of (oContMaps (X,Z)) /\ [: the carrier of XY, the carrier of XY:] by WELLORD1:def 6;
the InternalRel of XY = the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY
proof
the InternalRel of XY c= the InternalRel of (oContMaps (X,Z)) by YELLOW_0:def 13;
hence the InternalRel of XY c= the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY by ; :: according to XBOOLE_0:def 10 :: thesis: the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY c= the InternalRel of XY
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY or [x,y] in the InternalRel of XY )
assume A6: [x,y] in the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY ; :: thesis: [x,y] in the InternalRel of XY
then A7: [x,y] in [: the carrier of XY, the carrier of XY:] by ;
reconsider x = x, y = y as Element of XY by ;
the carrier of XY c= the carrier of (oContMaps (X,Z)) by YELLOW_0:def 13;
then reconsider a = x, b = y as Element of (oContMaps (X,Z)) ;
reconsider f9 = a, g9 = b as continuous Function of X,() by Th1;
reconsider f = x, g = y as continuous Function of X,() by Th1;
[a,b] in the InternalRel of (oContMaps (X,Z)) by ;
then a <= b by ORDERS_2:def 5;
then f9 <= g9 by Th3;
then f <= g by ;
then x <= y by Th3;
hence [x,y] in the InternalRel of XY by ORDERS_2:def 5; :: thesis: verum
end;
hence oContMaps (X,Y) is full SubRelStr of oContMaps (X,Z) by YELLOW_0:def 14; :: thesis: verum