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