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