let L be complete LATTICE; 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; 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); ( x = c1 & y = c2 implies ( x <= y iff c1 <= c2 ) )
assume that
A1:
x = c1
and
A2:
y = c2
; ( x <= y iff c1 <= c2 )
reconsider x9 = x, y9 = y as Element of (MonMaps (L,L)) by YELLOW_0:58;
reconsider x99 = x9, y99 = y9 as Element of (L |^ the carrier of L) by YELLOW_0:58;
( x99 <= y99 iff x9 <= y9 )
by YELLOW_0:59, YELLOW_0:60;
hence
( x <= y iff c1 <= c2 )
by A1, A2, Th11, YELLOW_0:59, YELLOW_0:60; verum