let S, T be non empty TopPoset; for X being non empty filtered Subset of S
for f being monotone Function of S,T
for Y being non empty filtered Subset of T st Y = f .: X holds
f * (X opp+id) is subnet of Y opp+id
let X be non empty filtered Subset of S; for f being monotone Function of S,T
for Y being non empty filtered Subset of T st Y = f .: X holds
f * (X opp+id) is subnet of Y opp+id
let f be monotone Function of S,T; for Y being non empty filtered Subset of T st Y = f .: X holds
f * (X opp+id) is subnet of Y opp+id
let Y be non empty filtered Subset of T; ( Y = f .: X implies f * (X opp+id) is subnet of Y opp+id )
assume A1:
Y = f .: X
; f * (X opp+id) is subnet of Y opp+id
set N = f * (X opp+id);
set M = Y opp+id ;
A2:
RelStr(# the carrier of (f * (X opp+id)), the InternalRel of (f * (X opp+id)) #) = RelStr(# the carrier of (X opp+id), the InternalRel of (X opp+id) #)
by WAYBEL_9:def 8;
A3:
the mapping of (f * (X opp+id)) = f * the mapping of (X opp+id)
by WAYBEL_9:def 8;
A4:
the carrier of (Y opp+id) = Y
by YELLOW_9:7;
A5:
the mapping of (Y opp+id) = id Y
by WAYBEL19:27;
A6:
the carrier of (X opp+id) = X
by YELLOW_9:7;
the mapping of (X opp+id) = id X
by WAYBEL19:27;
then A7:
the mapping of (f * (X opp+id)) = f | X
by A3, RELAT_1:65;
then A8:
rng the mapping of (f * (X opp+id)) = f .: X
by RELAT_1:115;
dom the mapping of (f * (X opp+id)) = X
by A2, A6, FUNCT_2:def 1;
then reconsider g = f | X as Function of (f * (X opp+id)),(Y opp+id) by A1, A2, A4, A6, A7, A8, FUNCT_2:def 1, RELSET_1:4;
take
g
; YELLOW_6:def 9 ( the mapping of (f * (X opp+id)) = the mapping of (Y opp+id) * g & ( for b1 being Element of the carrier of (Y opp+id) ex b2 being Element of the carrier of (f * (X opp+id)) st
for b3 being Element of the carrier of (f * (X opp+id)) holds
( not b2 <= b3 or b1 <= g . b3 ) ) )
thus
the mapping of (f * (X opp+id)) = the mapping of (Y opp+id) * g
by A1, A5, A7, A8, RELAT_1:53; for b1 being Element of the carrier of (Y opp+id) ex b2 being Element of the carrier of (f * (X opp+id)) st
for b3 being Element of the carrier of (f * (X opp+id)) holds
( not b2 <= b3 or b1 <= g . b3 )
let m be Element of (Y opp+id); ex b1 being Element of the carrier of (f * (X opp+id)) st
for b2 being Element of the carrier of (f * (X opp+id)) holds
( not b1 <= b2 or m <= g . b2 )
consider n being object such that
A9:
n in the carrier of S
and
A10:
n in X
and
A11:
m = f . n
by A1, A4, FUNCT_2:64;
reconsider n = n as Element of (f * (X opp+id)) by A2, A10, YELLOW_9:7;
take
n
; for b1 being Element of the carrier of (f * (X opp+id)) holds
( not n <= b1 or m <= g . b1 )
let p be Element of (f * (X opp+id)); ( not n <= p or m <= g . p )
p in X
by A2, A6;
then reconsider n9 = n, p9 = p as Element of S by A9;
reconsider fp = f . p9 as Element of (Y opp+id) by A1, A2, A4, A6, FUNCT_2:35;
X opp+id is SubRelStr of S opp
by YELLOW_9:7;
then A12:
f * (X opp+id) is SubRelStr of S opp
by A2, Th12;
A13:
Y opp+id is full SubRelStr of T opp
by YELLOW_9:7;
assume
n <= p
; m <= g . p
then
n9 ~ <= p9 ~
by A12, YELLOW_0:59;
then
n9 >= p9
by LATTICE3:9;
then
f . n9 >= f . p9
by WAYBEL_1:def 2;
then
(f . n9) ~ <= (f . p9) ~
by LATTICE3:9;
then
fp >= m
by A11, A13, YELLOW_0:60;
hence
m <= g . p
by A2, A6, FUNCT_1:49; verum