let L be non empty RelStr ; :: thesis: ( L is complete iff L opp is complete )

A1: now :: thesis: for L being non empty RelStr st L is complete holds
L opp is complete

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 and
A4: 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;
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 A5: 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 ex z being Element of L st
( b = z & z is_<=_than X ) ;
hence b <= ~ y by A5; :: thesis: verum

end;

hence y <= x by Th2, A4; :: 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 A6: a >= ~ y by A3;
~ x = x ;
hence x <= y by A6, Th1; :: thesis: verum

end;

end;

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