let S be non empty TopSpace; :: thesis: for T being non empty TopSpace-like reflexive TopRelStr
for x, y being Element of (ContMaps (S,T)) holds
( x <= y iff for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T )
let T be non empty TopSpace-like reflexive TopRelStr ; :: thesis: for x, y being Element of (ContMaps (S,T)) holds
( x <= y iff for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T )
let x, y be Element of (ContMaps (S,T)); :: thesis: ( x <= y iff for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T )
A1: ContMaps (S,T) is full SubRelStr of T |^ the carrier of S by Def3;
then reconsider x9 = x, y9 = y as Element of (T |^ the carrier of S) by YELLOW_0:58;
reconsider xa = x9, ya = y9 as Function of S,T by Th19;
hereby :: thesis: ( ( for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T ) implies x <= y )
assume A2: x <= y ; :: thesis: for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T
let i be Element of S; :: thesis: [(x . i),(y . i)] in the InternalRel of T
x9 <= y9 by A1, A2, YELLOW_0:59;
then xa <= ya by WAYBEL10:11;
then ex a, b being Element of T st
( a = xa . i & b = ya . i & a <= b ) by YELLOW_2:def 1;
hence [(x . i),(y . i)] in the InternalRel of T ; :: thesis: verum
end;
assume A3: for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T ; :: thesis: x <= y
now :: thesis: for j being set st j in the carrier of S holds
ex a, b being Element of T st
( a = xa . j & b = ya . j & a <= b )
let j be set ; :: thesis: ( j in the carrier of S implies ex a, b being Element of T st
( a = xa . j & b = ya . j & a <= b ) )
assume j in the carrier of S ; :: thesis: ex a, b being Element of T st
( a = xa . j & b = ya . j & a <= b )
then reconsider i = j as Element of S ;
reconsider a = xa . i, b = ya . i as Element of T ;
take a = a; :: thesis: ex b being Element of T st
( a = xa . j & b = ya . j & a <= b )
take b = b; :: thesis: ( a = xa . j & b = ya . j & a <= b )
thus ( a = xa . j & b = ya . j ) ; :: thesis: a <= b
[a,b] in the InternalRel of T by A3;
hence a <= b ; :: thesis: verum
end;
then xa <= ya by YELLOW_2:def 1;
then x9 <= y9 by WAYBEL10:11;
hence x <= y by A1, YELLOW_0:60; :: thesis: verum