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 x' = x, y' = y as Element of (T |^ the carrier of S) by YELLOW_0:59;
reconsider xa = x', ya = y' 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 x <= y ; :: thesis: for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T
then x' <= y' by A1, YELLOW_0:60;
then A2: xa <= ya by WAYBEL10:12;
let i be Element of S; :: thesis: [(x . i),(y . i)] in the InternalRel of T
consider a, b being Element of T such that
A3: ( a = xa . i & b = ya . i & a <= b ) by A2, YELLOW_2:def 1;
thus [(x . i),(y . i)] in the InternalRel of T by A3, ORDERS_2:def 9; :: thesis: verum

end;

assume A4: for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T ; :: thesis: x <= y

now

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 A4;
hence a <= b by ORDERS_2:def 9; :: thesis: verum

end;

then xa <= ya by YELLOW_2:def 1;
then x' <= y' by WAYBEL10:12;
hence x <= y by A1, YELLOW_0:61; :: thesis: verum