let L be non empty Boolean RelStr ; :: thesis: 'not' (Top L) = Bottom L
A1: (Bottom L) "/\" (Top L) = Bottom L by WAYBEL_1:4;
(Bottom L) "\/" (Top L) = Top L by WAYBEL_1:5;
then Bottom L is_a_complement_of Top L by A1, WAYBEL_1:def 23;
hence 'not' (Top L) = Bottom L by Th11; :: thesis: verum