( A is with_suprema & A is with_infima ) by Th12;
then A1: RelStr(# the carrier of A, the InternalRel of A #) = LattPOSet (latt A) by Def15;
set B = LattPOSet (latt A);
latt A is complete

proof

let X be set ; :: according to LATTICE3:def 18 :: thesis: ex p being Element of (latt A) st
( X is_less_than p & ( for r being Element of (latt A) st X is_less_than r holds
p [= r ) )
consider a being Element of A such that
A2: X is_<=_than a and
A3: for b being Element of A st X is_<=_than b holds
a <= b by Def12;
reconsider a9 = a as Element of (LattPOSet (latt A)) by A1;
take p = % a9; :: thesis: ( X is_less_than p & ( for r being Element of (latt A) st X is_less_than r holds
p [= r ) )
A4: p % = p ;
thus X is_less_than p :: thesis: for r being Element of (latt A) st X is_less_than r holds
p [= r

proof

let q be Element of (latt A); :: according to LATTICE3:def 17 :: thesis: ( q in X implies q [= p )
reconsider b = q as Element of A by A1;
assume q in X ; :: thesis: q [= p
then b <= a by A2;
then [b,a] in the InternalRel of A ;
then q % <= a9 by A1;
hence q [= p by A4, Th7; :: thesis: verum

end;

let q be Element of (latt A); :: thesis: ( X is_less_than q implies p [= q )
assume X is_less_than q ; :: thesis: p [= q
then A5: X is_<=_than q % by Th30;
reconsider b = q % as Element of A by A1;
X is_<=_than b

proof

let c be Element of A; :: according to LATTICE3:def 9 :: thesis: ( c in X implies c <= b )
reconsider c9 = c as Element of (LattPOSet (latt A)) by A1;
assume c in X ; :: thesis: c <= b
then c9 <= q % by A5;
then [c,b] in the InternalRel of RelStr(# the carrier of A, the InternalRel of A #) by A1;
hence c <= b ; :: thesis: verum

end;

then a <= b by A3;
then [a,b] in the InternalRel of A ;
then a9 <= q % by A1;
hence p [= q by A4, Th7; :: thesis: verum

end;

hence latt A is complete ; :: thesis: verum