let S, T be non empty TopPoset; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( Y = f .: X implies f * (X opp+id) is subnet of Y opp+id )
assume A1: Y = f .: X ; :: thesis: 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 ; :: according to YELLOW_6:def 9 :: thesis: ( the mapping of (f * (X opp+id)) = the mapping of (Y opp+id) * g & ( for b₁ being Element of the carrier of (Y opp+id) ex b₂ being Element of the carrier of (f * (X opp+id)) st
for b₃ being Element of the carrier of (f * (X opp+id)) holds
( not b₂ <= b₃ or b₁ <= g . b₃ ) ) )
thus the mapping of (f * (X opp+id)) = the mapping of (Y opp+id) * g by A1, A5, A7, A8, RELAT_1:53; :: thesis: for b₁ being Element of the carrier of (Y opp+id) ex b₂ being Element of the carrier of (f * (X opp+id)) st
for b₃ being Element of the carrier of (f * (X opp+id)) holds
( not b₂ <= b₃ or b₁ <= g . b₃ )
let m be Element of (Y opp+id); :: thesis: ex b₁ being Element of the carrier of (f * (X opp+id)) st
for b₂ being Element of the carrier of (f * (X opp+id)) holds
( not b₁ <= b₂ or m <= g . b₂ )
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 ; :: thesis: for b₁ being Element of the carrier of (f * (X opp+id)) holds
( not n <= b₁ or m <= g . b₁ )
let p be Element of (f * (X opp+id)); :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum