A1: now

let L be non empty RelStr ; :: thesis: ( L is complete implies L opp is complete )
assume A2: L is complete ; :: thesis: L opp is complete
thus L opp is complete :: thesis: verum

proof

let X be set ; :: according to LATTICE3:def 12 :: thesis: ex b₁ being Element of the carrier of (L opp ) st
( X is_<=_than b₁ & ( for b₂ being Element of the carrier of (L opp ) holds
( not X is_<=_than b₂ or b₁ <= b₂ ) ) )
set Y = { x where x is Element of L : x is_<=_than X } ;
consider a being Element of L such that
A3: ( { x where x is Element of L : x is_<=_than X } is_<=_than a & ( for b being Element of L st { x where x is Element of L : x is_<=_than X } is_<=_than b holds
a <= b ) ) by A2, LATTICE3:def 12;
take x = a ~ ; :: thesis: ( X is_<=_than x & ( for b₁ being Element of the carrier of (L opp ) holds
( not X is_<=_than b₁ or x <= b₁ ) ) )
thus X is_<=_than x :: thesis: for b₁ being Element of the carrier of (L opp ) holds
( not X is_<=_than b₁ or x <= b₁ )

proof

let y be Element of (L opp ); :: according to LATTICE3:def 9 :: thesis: ( not y in X or y <= x )
assume A4: y in X ; :: thesis: y <= x
{ x where x is Element of L : x is_<=_than X } is_<=_than ~ y

proof

let b be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not b in { x where x is Element of L : x is_<=_than X } or b <= ~ y )
assume b in { x where x is Element of L : x is_<=_than X } ; :: thesis: b <= ~ y
then ( y = ~ y & ex z being Element of L st
( b = z & z is_<=_than X ) ) ;
hence b <= ~ y by A4, LATTICE3:def 8; :: thesis: verum

end;

then a <= ~ y by A3;
hence y <= x by Th2; :: thesis: verum

end;

let y be Element of (L opp ); :: thesis: ( not X is_<=_than y or x <= y )
assume X is_<=_than y ; :: thesis: x <= y
then X is_>=_than ~ y by Th9;
then ~ y in { x where x is Element of L : x is_<=_than X } ;
then ( a >= ~ y & ~ x = x & x = a ) by A3, LATTICE3:def 9;
hence x <= y by Th1; :: thesis: verum

end;

end;

let L be non empty RelStr ; :: thesis: ( L is complete iff L opp is complete )
( (L opp ) ~ is complete implies L is complete ) by YELLOW_0:3;
hence ( L is complete iff L opp is complete ) by A1; :: thesis: verum