let V, V9, C, C9 be set ; :: thesis: ( 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 ) ; :: thesis: 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 :: thesis: 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 ; :: thesis: ( [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)) ; :: thesis: [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; :: thesis: 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 :: thesis: 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 K

let x, y be object ; :: thesis: ( [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 ; :: thesis: [x,y] in the InternalRel of K
then 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; :: thesis: 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 :: thesis: 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 K

let x, y be object ; :: thesis: ( [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 ; :: thesis: [x,y] in the InternalRel of (SubstPoset (V9,C9)) |_2 the carrier of K
then 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; :: thesis: 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; :: thesis: verum