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)

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;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

now :: thesis: for x, y being Element of L holds

( x <= y iff (ComplMap L) . x <= (ComplMap L) . y )

hence
ComplMap L is isomorphic
by A2, WAYBEL_0:66; :: thesis: verum( 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;( (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