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