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

A3: corestr f = f by WAYBEL_1:32;
A4: Image f is strict full Sublattice of EqRelLATT A ;
A5: 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 A3, WAYBEL_6:1
.= ((corestr f) . x) "/\" ((corestr f) . y) by A3, A4, YELLOW_0:70 ; :: thesis: verum

end;

A6: corestr f is one-to-one by A1, WAYBEL_1:32;
Image f is Semilattice ;
then ((corestr f) . y) "/\" ((corestr f) . x) = (corestr f) . x by A2, YELLOW_5:10;
then (corestr f) . x = (corestr f) . (x "/\" y) by A5;
then A7: x = x "/\" y by A6, WAYBEL_1:def 1;
assume not x <= y ; :: thesis: contradiction
hence contradiction by A7, YELLOW_0:25; :: thesis: verum

end;

hence x <= y ; :: thesis: verum