let V, V9, C, C9 be set ; ( V c= V9 & C c= C9 implies SubstPoset (V,C) is full SubRelStr of SubstPoset (V9,C9) )
set K = SubstPoset (V,C);
set L = SubstPoset (V9,C9);
A1:
( the carrier of (SubstPoset (V,C)) = SubstitutionSet (V,C) & the carrier of (SubstPoset (V9,C9)) = SubstitutionSet (V9,C9) )
by SUBSTLAT:def 4;
assume
( V c= V9 & C c= C9 )
; SubstPoset (V,C) is full SubRelStr of SubstPoset (V9,C9)
then A2:
the carrier of (SubstPoset (V,C)) c= the carrier of (SubstPoset (V9,C9))
by A1, Th9;
now for a, b being object st [a,b] in the InternalRel of (SubstPoset (V,C)) holds
[a,b] in the InternalRel of (SubstPoset (V9,C9))let a,
b be
object ;
( [a,b] in the InternalRel of (SubstPoset (V,C)) implies [a,b] in the InternalRel of (SubstPoset (V9,C9)) )assume A3:
[a,b] in the
InternalRel of
(SubstPoset (V,C))
;
[a,b] in the InternalRel of (SubstPoset (V9,C9))then reconsider a9 =
a,
b9 =
b as
Element of
(SubstPoset (V,C)) by ZFMISC_1:87;
(
a in the
carrier of
(SubstPoset (V,C)) &
b in the
carrier of
(SubstPoset (V,C)) )
by A3, ZFMISC_1:87;
then reconsider a1 =
a,
b1 =
b as
Element of
(SubstPoset (V9,C9)) by A2;
a9 <= b9
by A3, ORDERS_2:def 5;
then
for
x being
set st
x in a9 holds
ex
y being
set st
(
y in b9 &
y c= x )
by Th12;
then
a1 <= b1
by Th12;
hence
[a,b] in the
InternalRel of
(SubstPoset (V9,C9))
by ORDERS_2:def 5;
verum end;
then
the InternalRel of (SubstPoset (V,C)) c= the InternalRel of (SubstPoset (V9,C9))
by RELAT_1:def 3;
then reconsider K = SubstPoset (V,C) as SubRelStr of SubstPoset (V9,C9) by A2, YELLOW_0:def 13;
now for x, y being object st [x,y] in the InternalRel of (SubstPoset (V9,C9)) |_2 the carrier of K holds
[x,y] in the InternalRel of Klet x,
y be
object ;
( [x,y] in the InternalRel of (SubstPoset (V9,C9)) |_2 the carrier of K implies [x,y] in the InternalRel of K )assume A4:
[x,y] in the
InternalRel of
(SubstPoset (V9,C9)) |_2 the
carrier of
K
;
[x,y] in the InternalRel of Kthen A5:
[x,y] in the
InternalRel of
(SubstPoset (V9,C9))
by XBOOLE_0:def 4;
then reconsider p =
x,
q =
y as
Element of
(SubstPoset (V9,C9)) by ZFMISC_1:87;
[x,y] in [: the carrier of K, the carrier of K:]
by A4, XBOOLE_0:def 4;
then reconsider p9 =
x,
q9 =
y as
Element of
K by ZFMISC_1:87;
p <= q
by A5, ORDERS_2:def 5;
then
for
a being
set st
a in p holds
ex
b being
set st
(
b in q &
b c= a )
by Th12;
then
p9 <= q9
by Th12;
hence
[x,y] in the
InternalRel of
K
by ORDERS_2:def 5;
verum end;
then A6:
the InternalRel of (SubstPoset (V9,C9)) |_2 the carrier of K c= the InternalRel of K
by RELAT_1:def 3;
now for x, y being object st [x,y] in the InternalRel of K holds
[x,y] in the InternalRel of (SubstPoset (V9,C9)) |_2 the carrier of Klet x,
y be
object ;
( [x,y] in the InternalRel of K implies [x,y] in the InternalRel of (SubstPoset (V9,C9)) |_2 the carrier of K )assume A7:
[x,y] in the
InternalRel of
K
;
[x,y] in the InternalRel of (SubstPoset (V9,C9)) |_2 the carrier of Kthen reconsider p =
x,
q =
y as
Element of
K by ZFMISC_1:87;
reconsider p9 =
p,
q9 =
q as
Element of
(SubstPoset (V9,C9)) by A2;
p <= q
by A7, ORDERS_2:def 5;
then
for
a being
set st
a in p holds
ex
b being
set st
(
b in q &
b c= a )
by Th12;
then
p9 <= q9
by Th12;
then
[p9,q9] in the
InternalRel of
(SubstPoset (V9,C9))
by ORDERS_2:def 5;
hence
[x,y] in the
InternalRel of
(SubstPoset (V9,C9)) |_2 the
carrier of
K
by A7, XBOOLE_0:def 4;
verum end;
then
the InternalRel of K c= the InternalRel of (SubstPoset (V9,C9)) |_2 the carrier of K
by RELAT_1:def 3;
then
the InternalRel of K = the InternalRel of (SubstPoset (V9,C9)) |_2 the carrier of K
by A6;
hence
SubstPoset (V,C) is full SubRelStr of SubstPoset (V9,C9)
by YELLOW_0:def 14; verum