let L, M be non empty RelStr ; :: thesis: ( L,M are_isomorphic & L is complete implies M is complete )
assume that
A1: L,M are_isomorphic and
A2: L is complete ; :: thesis: M is complete
M,L are_isomorphic by A1, WAYBEL_1:7;
then consider f being Function of M,L such that
A3: f is isomorphic by WAYBEL_1:def 8;
A4: f is one-to-one by A3;
A5: rng f = the carrier of L by A3, WAYBEL_0:66;
A6: dom f = the carrier of M by FUNCT_2:def 1;
let X be Subset of M; :: according to LATTICE5:def 2 :: thesis: ex b₁ being Element of the carrier of M st
( b₁ is_<=_than X & ( for b₂ being Element of the carrier of M holds
( not b₂ is_<=_than X or b₂ <= b₁ ) ) )
reconsider fX = f .: X as Subset of L ;
consider fa being Element of L such that
A7: fa is_<=_than fX and
A8: for fb being Element of L st fb is_<=_than fX holds
fb <= fa by A2, LATTICE5:def 2;
set a = (f " ) . fa;
(f " ) . fa in dom f by A4, A5, FUNCT_1:54;
then reconsider a = (f " ) . fa as Element of M ;
A9: fa = f . a by A4, A5, FUNCT_1:57;
take a ; :: thesis: ( a is_<=_than X & ( for b₁ being Element of the carrier of M holds
( not b₁ is_<=_than X or b₁ <= a ) ) )

hereby :: according to LATTICE3:def 8 :: thesis: for b₁ being Element of the carrier of M holds
( not b₁ is_<=_than X or b₁ <= a )

let b be Element of M; :: thesis: ( b in X implies a <= b )
assume A10: b in X ; :: thesis: a <= b
reconsider fb = f . b as Element of L ;
fb in fX by A6, A10, FUNCT_1:def 12;
then fa <= fb by A7, LATTICE3:def 8;
hence a <= b by A3, A9, WAYBEL_0:66; :: thesis: verum

end;

let b be Element of M; :: thesis: ( not b is_<=_than X or b <= a )
assume A11: b is_<=_than X ; :: thesis: b <= a
reconsider fb = f . b as Element of L ;
fb is_<=_than fX

proof

let fc be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not fc in fX or fb <= fc )
assume fc in fX ; :: thesis: fb <= fc
then consider c being set such that
A12: ( c in dom f & c in X & fc = f . c ) by FUNCT_1:def 12;
reconsider c = c as Element of M by A12;
b <= c by A11, A12, LATTICE3:def 8;
hence fb <= fc by A3, A12, WAYBEL_0:66; :: thesis: verum

end;

then fb <= fa by A8;
hence b <= a by A3, A9, WAYBEL_0:66; :: thesis: verum