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 that

A1: x = c1 and

A2: y = c2 ; :: thesis: ( 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; :: thesis: verum

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 that

A1: x = c1 and

A2: y = c2 ; :: thesis: ( 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; :: thesis: verum