let a, b be Element of S; :: thesis: ( a is_a_complement_of b implies b is_a_complement_of a )
assume a is_a_complement_of b ; :: thesis: b is_a_complement_of a
hence ( a "\/" b = Top S & a "/\" b = Bottom S ) by WAYBEL_1:def 23; :: according to WAYBEL_1:def 23 :: thesis: verum