set f = ComplMap L;
let a, b be Element of L; :: according to WAYBEL_1:def 1 :: thesis: ( not (ComplMap L) . a = (ComplMap L) . b or a = b )
( (ComplMap L) . a = 'not' a & (ComplMap L) . b = 'not' b & 'not' ('not' a) = a & 'not' ('not' b) = b ) by Def1, WAYBEL_1:90;
hence ( not (ComplMap L) . a = (ComplMap L) . b or a = b ) ; :: thesis: verum