let L, M be complete LATTICE; :: thesis: for f being Function of L,M st ( f is sups-preserving or f is infs-preserving ) holds
Image f is complete LATTICE
let f be Function of L,M; :: thesis: ( ( f is sups-preserving or f is infs-preserving ) implies Image f is complete LATTICE )
assume A1: ( f is sups-preserving or f is infs-preserving ) ; :: thesis: Image f is complete LATTICE

per cases ( f is sups-preserving or f is infs-preserving ) by A1;

suppose f is sups-preserving ; :: thesis: Image f is complete LATTICE

then Image f is sups-inheriting by Th32;
hence Image f is complete LATTICE by Th31; :: thesis: verum

end;

suppose f is infs-preserving ; :: thesis: Image f is complete LATTICE

then Image f is infs-inheriting by Th33;
hence Image f is complete LATTICE by Th30; :: thesis: verum

end;

end;