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