set S = subrelstr (rng f);
A1:
the carrier of (subrelstr (rng f)) = rng f
by YELLOW_0:def 15;
A2:
dom f = the carrier of L1
by FUNCT_2:def 1;
for x, y being Element of L2 st x in the carrier of (subrelstr (rng f)) & y in the carrier of (subrelstr (rng f)) & ex_sup_of {x,y},L2 holds
sup {x,y} in the carrier of (subrelstr (rng f))
proof
let x,
y be
Element of
L2;
( x in the carrier of (subrelstr (rng f)) & y in the carrier of (subrelstr (rng f)) & ex_sup_of {x,y},L2 implies sup {x,y} in the carrier of (subrelstr (rng f)) )
assume that A3:
x in the
carrier of
(subrelstr (rng f))
and A4:
y in the
carrier of
(subrelstr (rng f))
and
ex_sup_of {x,y},
L2
;
sup {x,y} in the carrier of (subrelstr (rng f))
consider a being
object such that A5:
a in dom f
and A6:
x = f . a
by A1, A3, FUNCT_1:def 3;
consider b being
object such that A7:
b in dom f
and A8:
y = f . b
by A1, A4, FUNCT_1:def 3;
reconsider a9 =
a,
b9 =
b as
Element of
L1 by A5, A7;
A9:
(
f preserves_sup_of {a9,b9} &
ex_sup_of {a9,b9},
L1 )
by WAYBEL_0:def 35, YELLOW_0:20;
sup {x,y} =
sup (f .: {a9,b9})
by A5, A6, A7, A8, FUNCT_1:60
.=
f . (sup {a9,b9})
by A9
;
hence
sup {x,y} in the
carrier of
(subrelstr (rng f))
by A1, A2, FUNCT_1:def 3;
verum
end;
then A10:
subrelstr (rng f) is join-inheriting
by YELLOW_0:def 17;
for x, y being Element of L2 st x in the carrier of (subrelstr (rng f)) & y in the carrier of (subrelstr (rng f)) & ex_inf_of {x,y},L2 holds
inf {x,y} in the carrier of (subrelstr (rng f))
proof
let x,
y be
Element of
L2;
( x in the carrier of (subrelstr (rng f)) & y in the carrier of (subrelstr (rng f)) & ex_inf_of {x,y},L2 implies inf {x,y} in the carrier of (subrelstr (rng f)) )
assume that A11:
x in the
carrier of
(subrelstr (rng f))
and A12:
y in the
carrier of
(subrelstr (rng f))
and
ex_inf_of {x,y},
L2
;
inf {x,y} in the carrier of (subrelstr (rng f))
consider a being
object such that A13:
a in dom f
and A14:
x = f . a
by A1, A11, FUNCT_1:def 3;
consider b being
object such that A15:
b in dom f
and A16:
y = f . b
by A1, A12, FUNCT_1:def 3;
reconsider a9 =
a,
b9 =
b as
Element of
L1 by A13, A15;
A17:
(
f preserves_inf_of {a9,b9} &
ex_inf_of {a9,b9},
L1 )
by WAYBEL_0:def 34, YELLOW_0:21;
inf {x,y} =
inf (f .: {a9,b9})
by A13, A14, A15, A16, FUNCT_1:60
.=
f . (inf {a9,b9})
by A17
;
hence
inf {x,y} in the
carrier of
(subrelstr (rng f))
by A1, A2, FUNCT_1:def 3;
verum
end;
then
subrelstr (rng f) is meet-inheriting
by YELLOW_0:def 16;
hence
( Image f is meet-inheriting & Image f is join-inheriting )
by A10, YELLOW_2:def 2; verum