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 )

let x be Element of L; :: according to WAYBEL_1:def 24 :: thesis: ex b_{1} being Element of the carrier of L st b_{1} 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

thus ( L is complemented implies L opp is complemented ) :: thesis: ( L opp is complemented implies L is complemented )

proof

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
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_{1} being Element of the carrier of (L opp) st b_{1} 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;let x be Element of (L opp); :: according to WAYBEL_1:def 24 :: thesis: ex b

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

let x be Element of L; :: according to WAYBEL_1:def 24 :: thesis: ex b

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