let L be non empty Boolean RelStr ; :: thesis: for a being Element of L holds
( a "/\" ('not' a) = Bottom L & a "\/" ('not' a) = Top L )
let a be Element of L; :: thesis: ( a "/\" ('not' a) = Bottom L & a "\/" ('not' a) = Top L )
'not' a is_a_complement_of a by Th11;
hence ( a "/\" ('not' a) = Bottom L & a "\/" ('not' a) = Top L ) by WAYBEL_1:def 23; :: thesis: verum