let S be non empty TopSpace; :: thesis: for T being non empty TopSpace-like reflexive TopRelStr
for x, y being Element of holds
( x <= y iff for i being Element of 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 holds
( x <= y iff for i being Element of holds [(x . i),(y . i)] in the InternalRel of T )
let x, y be Element of ; :: thesis: ( x <= y iff for i being Element of 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 by YELLOW_0:59;
reconsider xa = x', ya = y' as Function of S,T by Th19;

hereby :: thesis: ( ( for i being Element of holds [(x . i),(y . i)] in the InternalRel of T ) implies x <= y )

assume A2: x <= y ; :: thesis: for i being Element of holds [(x . i),(y . i)] in the InternalRel of T
let i be Element of ; :: thesis: [(x . i),(y . i)] in the InternalRel of T
x' <= y' by A1, A2, YELLOW_0:60;
then xa <= ya by WAYBEL10:12;
then ex a, b being Element of st
( a = xa . i & b = ya . i & a <= b ) by YELLOW_2:def 1;
hence [(x . i),(y . i)] in the InternalRel of T by ORDERS_2:def 9; :: thesis: verum

end;

assume A3: for i being Element of 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 st
( a = xa . j & b = ya . j & a <= b ) )
assume j in the carrier of S ; :: thesis: ex a, b being Element of st
( a = xa . j & b = ya . j & a <= b )
then reconsider i = j as Element of ;
reconsider a = xa . i, b = ya . i as Element of ;
take a = a; :: thesis: ex b being Element of 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 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