let L2 be Lattice; :: thesis: for 1L being upper-bounded Lattice

for f being Homomorphism of 1L,L2 st f is onto holds

( L2 is upper-bounded & f preserves_top )

let 1L be upper-bounded Lattice; :: thesis: for f being Homomorphism of 1L,L2 st f is onto holds

( L2 is upper-bounded & f preserves_top )

let f be Homomorphism of 1L,L2; :: thesis: ( f is onto implies ( L2 is upper-bounded & f preserves_top ) )

set r = f . (Top 1L);

assume A1: f is onto ; :: thesis: ( L2 is upper-bounded & f preserves_top )

then Top L2 = f . (Top 1L) by A2, LATTICES:def 17;

hence f preserves_top ; :: thesis: verum

for f being Homomorphism of 1L,L2 st f is onto holds

( L2 is upper-bounded & f preserves_top )

let 1L be upper-bounded Lattice; :: thesis: for f being Homomorphism of 1L,L2 st f is onto holds

( L2 is upper-bounded & f preserves_top )

let f be Homomorphism of 1L,L2; :: thesis: ( f is onto implies ( L2 is upper-bounded & f preserves_top ) )

set r = f . (Top 1L);

assume A1: f is onto ; :: thesis: ( L2 is upper-bounded & f preserves_top )

A2: now :: thesis: for a2 being Element of L2 holds

( (f . (Top 1L)) "\/" a2 = f . (Top 1L) & a2 "\/" (f . (Top 1L)) = f . (Top 1L) )

thus
L2 is upper-bounded
by A2; :: thesis: f preserves_top ( (f . (Top 1L)) "\/" a2 = f . (Top 1L) & a2 "\/" (f . (Top 1L)) = f . (Top 1L) )

let a2 be Element of L2; :: thesis: ( (f . (Top 1L)) "\/" a2 = f . (Top 1L) & a2 "\/" (f . (Top 1L)) = f . (Top 1L) )

consider a1 being Element of 1L such that

A3: f . a1 = a2 by A1, Th6;

thus (f . (Top 1L)) "\/" a2 = f . ((Top 1L) "\/" a1) by A3, D1

.= f . (Top 1L) ; :: thesis: a2 "\/" (f . (Top 1L)) = f . (Top 1L)

hence a2 "\/" (f . (Top 1L)) = f . (Top 1L) ; :: thesis: verum

end;consider a1 being Element of 1L such that

A3: f . a1 = a2 by A1, Th6;

thus (f . (Top 1L)) "\/" a2 = f . ((Top 1L) "\/" a1) by A3, D1

.= f . (Top 1L) ; :: thesis: a2 "\/" (f . (Top 1L)) = f . (Top 1L)

hence a2 "\/" (f . (Top 1L)) = f . (Top 1L) ; :: thesis: verum

then Top L2 = f . (Top 1L) by A2, LATTICES:def 17;

hence f preserves_top ; :: thesis: verum