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 y is_a_complement_of x ; :: thesis: y ~ is_a_complement_of x ~
then A1: ( x "\/" y = Top L & x "/\" y = Bottom L ) by WAYBEL_1:def 23;
thus y ~ is_a_complement_of x ~ :: thesis: verum

proof

thus (x ~ ) "\/" (y ~ ) = (Bottom L) ~ by A1, Th21
.= Top (L opp ) by Th33 ; :: according to WAYBEL_1:def 23 :: thesis: (x ~ ) "/\" (y ~ ) = Bottom (L opp )
thus (x ~ ) "/\" (y ~ ) = (Top L) ~ by A1, Th23
.= Bottom (L opp ) by Th34 ; :: thesis: verum

end;

end;

assume A2: ( (x ~ ) "\/" (y ~ ) = Top (L opp ) & (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 A2, Th34
.= Top L ; :: according to WAYBEL_1:def 23 :: thesis: x "/\" y = Bottom L
thus x "/\" y = (x ~ ) "\/" (y ~ ) by Th21
.= (Bottom L) ~ by A2, Th33
.= Bottom L ; :: thesis: verum