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_inf_of {x,y},L2 holds
inf {x,y} in the carrier of (subrelstr (rng f))
proof
let x,
y be
Element of
L2;
:: thesis: ( 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 A3:
(
x in the
carrier of
(subrelstr (rng f)) &
y in the
carrier of
(subrelstr (rng f)) &
ex_inf_of {x,y},
L2 )
;
:: thesis: inf {x,y} in the carrier of (subrelstr (rng f))
then consider a being
set such that A4:
(
a in dom f &
x = f . a )
by A1, FUNCT_1:def 5;
consider b being
set such that A5:
(
b in dom f &
y = f . b )
by A1, A3, FUNCT_1:def 5;
reconsider a' =
a,
b' =
b as
Element of
L1 by A4, A5;
A6:
f preserves_inf_of {a',b'}
by WAYBEL_0:def 34;
A7:
ex_inf_of {a',b'},
L1
by YELLOW_0:21;
inf {x,y} =
inf (f .: {a',b'})
by A4, A5, FUNCT_1:118
.=
f . (inf {a',b'})
by A6, A7, WAYBEL_0:def 30
;
hence
inf {x,y} in the
carrier of
(subrelstr (rng f))
by A1, A2, FUNCT_1:def 5;
:: thesis: verum
end;
then A8:
subrelstr (rng f) is meet-inheriting
by YELLOW_0:def 16;
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;
:: thesis: ( 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 A9:
(
x in the
carrier of
(subrelstr (rng f)) &
y in the
carrier of
(subrelstr (rng f)) &
ex_sup_of {x,y},
L2 )
;
:: thesis: sup {x,y} in the carrier of (subrelstr (rng f))
then consider a being
set such that A10:
(
a in dom f &
x = f . a )
by A1, FUNCT_1:def 5;
consider b being
set such that A11:
(
b in dom f &
y = f . b )
by A1, A9, FUNCT_1:def 5;
reconsider a' =
a,
b' =
b as
Element of
L1 by A10, A11;
A12:
f preserves_sup_of {a',b'}
by WAYBEL_0:def 35;
A13:
ex_sup_of {a',b'},
L1
by YELLOW_0:20;
sup {x,y} =
sup (f .: {a',b'})
by A10, A11, FUNCT_1:118
.=
f . (sup {a',b'})
by A12, A13, WAYBEL_0:def 31
;
hence
sup {x,y} in the
carrier of
(subrelstr (rng f))
by A1, A2, FUNCT_1:def 5;
:: thesis: verum
end;
then
subrelstr (rng f) is join-inheriting
by YELLOW_0:def 17;
hence
Image f is strict full Sublattice of L2
by A8, YELLOW_2:def 2; :: thesis: verum