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:
let x be Element of (L opp); :: according to WAYBEL_1:def 24 :: thesis: ex b1 being Element of the carrier of (L opp) st b1 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:
(~ x) ~ = ~ x ;
hence y ~ is_a_complement_of x by ; :: 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 b1 being Element of the carrier of L st b1 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) ~ = ~ y ;
hence ~ y is_a_complement_of x by ; :: thesis: verum