let S be non empty TopSpace; :: thesis: for T being non empty TopSpace-like TopRelStr
for f, g being Function of S,T
for x, y being Element of (ContMaps (S,T)) st x = f & y = g holds
( x <= y iff f <= g )
let T be non empty TopSpace-like TopRelStr ; :: thesis: for f, g being Function of S,T
for x, y being Element of (ContMaps (S,T)) st x = f & y = g holds
( x <= y iff f <= g )
let f, g be Function of S,T; :: thesis: for x, y being Element of (ContMaps (S,T)) st x = f & y = g holds
( x <= y iff f <= g )
let x, y be Element of (ContMaps (S,T)); :: thesis: ( x = f & y = g implies ( x <= y iff f <= g ) )
assume A1: ( x = f & y = g ) ; :: thesis: ( x <= y iff f <= g )
A2: ContMaps (S,T) is full SubRelStr of T |^ the carrier of S by WAYBEL24:def 3;
then reconsider x1 = x, y1 = y as Element of (T |^ the carrier of S) by YELLOW_0:58;

hereby :: thesis: ( f <= g implies x <= y )

assume x <= y ; :: thesis: f <= g
then x1 <= y1 by A2, YELLOW_0:59;
hence f <= g by A1, WAYBEL10:11; :: thesis: verum

end;

assume f <= g ; :: thesis: x <= y
then x1 <= y1 by A1, WAYBEL10:11;
hence x <= y by A2, YELLOW_0:60; :: thesis: verum