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 ~ )

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

( 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 that 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;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

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