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 object ; :: 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:87;
then (ComplMap L) . ('not' x) = x by Def1;
hence x in rng (ComplMap L) by A1, FUNCT_1:def 3; :: thesis: verum

end;

now :: thesis: for x, y being Element of L holds
( x <= y iff (ComplMap L) . x <= (ComplMap L) . y )

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 A3: ( 'not' x >= 'not' y iff (ComplMap L) . x <= (ComplMap L) . y ) by LATTICE3:9;
( x = 'not' ('not' x) & y = 'not' ('not' y) ) by WAYBEL_1:87;
hence ( x <= y iff (ComplMap L) . x <= (ComplMap L) . y ) by A3, WAYBEL_1:83; :: thesis: verum

end;

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