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 x "/\" y = Bottom L by WAYBEL_1:def 23;
then A2: (x ~ ) "\/" (y ~ ) = (Bottom L) ~ by Th21
.= Top (L opp ) by Th12, YELLOW_0:42 ;
x "\/" y = Top L by A1, WAYBEL_1:def 23;
then (x ~ ) "/\" (y ~ ) = (Top L) ~ by Th23
.= Bottom (L opp ) by Th13, YELLOW_0:43 ;
hence y ~ is_a_complement_of x ~ by A2, WAYBEL_1:def 23; :: 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
.= Top L ; :: 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
.= Bottom L ; :: thesis: verum