let L be bounded LATTICE; :: thesis: for x, y being Element of L holds
( y is_a_complement_of x iff y ~ is_a_complement_of x ~ )
let x, y be Element of L; :: thesis: ( y is_a_complement_of x iff y ~ is_a_complement_of x ~ )

hereby :: thesis: ( y ~ is_a_complement_of x ~ implies y is_a_complement_of x )

assume A1: y is_a_complement_of x ; :: thesis: y ~ is_a_complement_of x ~
then A2: (x ~) "\/" (y ~) = (Bottom L) ~ by Th21
.= Top (L opp) by Th12, YELLOW_0:42 ;
(x ~) "/\" (y ~) = (Top L) ~ by Th23, A1
.= Bottom (L opp) by Th13, YELLOW_0:43 ;
hence y ~ is_a_complement_of x ~ by A2; :: thesis: verum

end;

assume that
A3: (x ~) "\/" (y ~) = Top (L opp) and
A4: (x ~) "/\" (y ~) = Bottom (L opp) ; :: according to WAYBEL_1:def 23 :: thesis: y is_a_complement_of x
thus x "\/" y = (x ~) "/\" (y ~) by Th23
.= Top L by A4, Th13, YELLOW_0:43 ; :: according to WAYBEL_1:def 23 :: thesis: x "/\" y = Bottom L
thus x "/\" y = (x ~) "\/" (y ~) by Th21
.= Bottom L by A3, Th12, YELLOW_0:42 ; :: thesis: verum