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

hence ( L is complete iff L opp is complete ) by A1; :: thesis: verum

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

L opp is complete

( (L opp) ~ is complete implies L is complete )
by YELLOW_0:3;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

end;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_{1} being Element of the carrier of (L opp) st

( X is_<=_than b_{1} & ( for b_{2} being Element of the carrier of (L opp) holds

( not X is_<=_than b_{2} or b_{1} <= b_{2} ) ) )

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_{1} being Element of the carrier of (L opp) holds

( not X is_<=_than b_{1} or x <= b_{1} ) ) )

thus X is_<=_than x :: thesis: for b_{1} being Element of the carrier of (L opp) holds

( not X is_<=_than b_{1} or x <= b_{1} )

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;( X is_<=_than b

( not X is_<=_than 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

( not X is_<=_than b

thus X is_<=_than x :: thesis: for b

( not X is_<=_than b

proof

let y be Element of (L opp); :: thesis: ( not X is_<=_than y or x <= y )
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

end;assume A5: y in X ; :: thesis: y <= x

{ x where x is Element of L : x is_<=_than X } is_<=_than ~ y

proof

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

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

hence ( L is complete iff L opp is complete ) by A1; :: thesis: verum