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 :: thesis: x <= y

A3: corestr f = f by WAYBEL_1:30;
A4: 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, YELLOW_0:69 ; :: thesis: verum

end;

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

end;

hence x <= y ; :: thesis: verum