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
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₁ ) ) )
M,L are_isomorphic by A1, WAYBEL_1:6;
then consider f being Function of M,L such that
A3: f is isomorphic ;
reconsider fX = f .: X as Subset of L ;
consider fa being Element of L such that
A4: fa is_<=_than fX and
A5: for fb being Element of L st fb is_<=_than fX holds
fb <= fa by A2;
set a = (f ") . fa;
A6: rng f = the carrier of L by A3, WAYBEL_0:66;
then (f ") . fa in dom f by A3, FUNCT_1:32;
then reconsider a = (f ") . fa as Element of M ;
A7: fa = f . a by A3, A6, FUNCT_1:35;
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 ) ) )
A8: dom f = the carrier of M by FUNCT_2:def 1;

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 A9: b in X ; :: thesis: a <= b
reconsider fb = f . b as Element of L ;
fb in fX by A8, A9, FUNCT_1:def 6;
then fa <= fb by A4;
hence a <= b by A3, A7, WAYBEL_0:66; :: thesis: verum

end;

let b be Element of M; :: thesis: ( not b is_<=_than X or b <= a )
assume A10: 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 object such that
A11: c in dom f and
A12: c in X and
A13: fc = f . c by FUNCT_1:def 6;
reconsider c = c as Element of M by A11;
b <= c by A10, A12;
hence fb <= fc by A3, A13, WAYBEL_0:66; :: thesis: verum

end;

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