set f = ComplMap L;
A1: dom (ComplMap L) = the carrier of L by FUNCT_2:def 1;
A2: rng (ComplMap L) = the carrier of (L opp )

proof

thus rng (ComplMap L) c= the carrier of (L opp ) ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of (L opp ) c= rng (ComplMap L)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (L opp ) or x in rng (ComplMap L) )
assume x in the carrier of (L opp ) ; :: thesis: x in rng (ComplMap L)
then reconsider x = x as Element of L ;
x = 'not' ('not' x) by WAYBEL_1:90;
then (ComplMap L) . ('not' x) = x by Def1;
hence x in rng (ComplMap L) by A1, FUNCT_1:def 5; :: thesis: verum

end;

now

let x, y be Element of L; :: thesis: ( x <= y iff (ComplMap L) . x <= (ComplMap L) . y )
( (ComplMap L) . x = ('not' x) ~ & (ComplMap L) . y = ('not' y) ~ ) by Def1;
then ( ( 'not' x >= 'not' y implies (ComplMap L) . x <= (ComplMap L) . y ) & ( (ComplMap L) . x <= (ComplMap L) . y implies 'not' x >= 'not' y ) & x = 'not' ('not' x) & y = 'not' ('not' y) ) by LATTICE3:9, WAYBEL_1:90;
hence ( x <= y iff (ComplMap L) . x <= (ComplMap L) . y ) by WAYBEL_1:86; :: thesis: verum

end;

hence ComplMap L is isomorphic by A2, WAYBEL_0:66; :: thesis: verum