let L be lower-bounded LATTICE; :: thesis: for x, y being Element of L
for A being non empty set
for f being Homomorphism of L,(EqRelLATT A) st f is one-to-one & (corestr f) . x <= (corestr f) . y holds
x <= y
let x, y be Element of L; :: thesis: for A being non empty set
for f being Homomorphism of L,(EqRelLATT A) st f is one-to-one & (corestr f) . x <= (corestr f) . y holds
x <= y
let A be non empty set ; :: thesis: for f being Homomorphism of L,(EqRelLATT A) st f is one-to-one & (corestr f) . x <= (corestr f) . y holds
x <= y
let f be Homomorphism of L,(EqRelLATT A); :: thesis: ( f is one-to-one & (corestr f) . x <= (corestr f) . y implies x <= y )
assume that
A1: f is one-to-one and
A2: (corestr f) . x <= (corestr f) . y ; :: thesis: x <= y

now

assume A3: not x <= y ; :: thesis: contradiction
A4: ( corestr f = f & corestr f is one-to-one ) by A1, WAYBEL_1:32;
A5: ( Image f is Semilattice & L is Semilattice ) ;
A6: Image f is strict full Sublattice of EqRelLATT A ;
A7: for x, y being Element of L holds (corestr f) . (x "/\" y) = ((corestr f) . x) "/\" ((corestr f) . y)

proof

let x, y be Element of L; :: thesis: (corestr f) . (x "/\" y) = ((corestr f) . x) "/\" ((corestr f) . y)
thus (corestr f) . (x "/\" y) = (f . x) "/\" (f . y) by A4, WAYBEL_6:1
.= ((corestr f) . x) "/\" ((corestr f) . y) by A4, A6, YELLOW_0:70 ; :: thesis: verum

end;

((corestr f) . y) "/\" ((corestr f) . x) = (corestr f) . x by A2, A5, YELLOW_5:10;
then (corestr f) . x = (corestr f) . (x "/\" y) by A7;
then x = x "/\" y by A4, WAYBEL_1:def 1;
hence contradiction by A3, YELLOW_0:25; :: thesis: verum

end;

hence x <= y ; :: thesis: verum