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