let L be bounded LATTICE; :: thesis: ( L is complemented iff L opp is complemented )
thus ( L is complemented implies L opp is complemented ) :: thesis: ( L opp is complemented implies L is complemented )

proof

assume A1: for x being Element of L ex y being Element of L st y is_a_complement_of x ; :: according to WAYBEL_1:def 24 :: thesis: L opp is complemented
let x be Element of (L opp); :: according to WAYBEL_1:def 24 :: thesis: ex b₁ being Element of the carrier of (L opp) st b₁ is_a_complement_of x
consider y being Element of L such that
A2: y is_a_complement_of ~ x by A1;
take y ~ ; :: thesis: y ~ is_a_complement_of x
(~ x) ~ = ~ x ;
hence y ~ is_a_complement_of x by A2, Th35; :: thesis: verum

end;

assume A3: for x being Element of (L opp) ex y being Element of (L opp) st y is_a_complement_of x ; :: according to WAYBEL_1:def 24 :: thesis: L is complemented
let x be Element of L; :: according to WAYBEL_1:def 24 :: thesis: ex b₁ being Element of the carrier of L st b₁ is_a_complement_of x
consider y being Element of (L opp) such that
A4: y is_a_complement_of x ~ by A3;
take ~ y ; :: thesis: ~ y is_a_complement_of x
(~ y) ~ = ~ y ;
hence ~ y is_a_complement_of x by A4, Th35; :: thesis: verum