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