let L be complete LATTICE; :: thesis: for c1, c2 being Function of L,L
for x, y being Element of (ClOpers L) st x = c1 & y = c2 holds
( x <= y iff c1 <= c2 )
let c1, c2 be Function of L,L; :: thesis: for x, y being Element of (ClOpers L) st x = c1 & y = c2 holds
( x <= y iff c1 <= c2 )
let x, y be Element of (ClOpers L); :: thesis: ( x = c1 & y = c2 implies ( x <= y iff c1 <= c2 ) )
assume A1: ( x = c1 & y = c2 ) ; :: thesis: ( x <= y iff c1 <= c2 )
reconsider x' = x, y' = y as Element of (MonMaps L,L) by YELLOW_0:59;
reconsider x'' = x', y'' = y' as Element of (L |^ the carrier of L) by YELLOW_0:59;
( x'' <= y'' iff x' <= y' ) by YELLOW_0:60, YELLOW_0:61;
hence ( x <= y iff c1 <= c2 ) by A1, Th12, YELLOW_0:60, YELLOW_0:61; :: thesis: verum