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