let V, V', C, C' be set ; :: thesis: ( V c= V' & C c= C' implies SubstPoset V,C is full SubRelStr of SubstPoset V',C' )
set K = SubstPoset V,C;
set L = SubstPoset V',C';
A1: ( the carrier of (SubstPoset V,C) = SubstitutionSet V,C & the carrier of (SubstPoset V',C') = SubstitutionSet V',C' ) by SUBSTLAT:def 4;
assume ( V c= V' & C c= C' ) ; :: thesis: SubstPoset V,C is full SubRelStr of SubstPoset V',C'
then A2: the carrier of (SubstPoset V,C) c= the carrier of (SubstPoset V',C') by A1, Th12;

now

let a, b be set ; :: thesis: ( [a,b] in the InternalRel of (SubstPoset V,C) implies [a,b] in the InternalRel of (SubstPoset V',C') )
assume A3: [a,b] in the InternalRel of (SubstPoset V,C) ; :: thesis: [a,b] in the InternalRel of (SubstPoset V',C')
then reconsider a' = a, b' = b as Element of by ZFMISC_1:106;
( a in the carrier of (SubstPoset V,C) & b in the carrier of (SubstPoset V,C) ) by A3, ZFMISC_1:106;
then reconsider a1 = a, b1 = b as Element of by A2;
a' <= b' by A3, ORDERS_2:def 9;
then for x being set st x in a' holds
ex y being set st
( y in b' & y c= x ) by Th15;
then a1 <= b1 by Th15;
hence [a,b] in the InternalRel of (SubstPoset V',C') by ORDERS_2:def 9; :: thesis: verum

end;

then the InternalRel of (SubstPoset V,C) c= the InternalRel of (SubstPoset V',C') by RELAT_1:def 3;
then reconsider K = SubstPoset V,C as SubRelStr of SubstPoset V',C' by A2, YELLOW_0:def 13;

now

let x, y be set ; :: thesis: ( [x,y] in the InternalRel of (SubstPoset V',C') |_2 the carrier of K implies [x,y] in the InternalRel of K )
assume A4: [x,y] in the InternalRel of (SubstPoset V',C') |_2 the carrier of K ; :: thesis: [x,y] in the InternalRel of K
then A5: [x,y] in the InternalRel of (SubstPoset V',C') by XBOOLE_0:def 4;
then reconsider p = x, q = y as Element of by ZFMISC_1:106;
[x,y] in [:the carrier of K,the carrier of K:] by A4, XBOOLE_0:def 4;
then reconsider p' = x, q' = y as Element of by ZFMISC_1:106;
p <= q by A5, ORDERS_2:def 9;
then for a being set st a in p holds
ex b being set st
( b in q & b c= a ) by Th15;
then p' <= q' by Th15;
hence [x,y] in the InternalRel of K by ORDERS_2:def 9; :: thesis: verum

end;

then A6: the InternalRel of (SubstPoset V',C') |_2 the carrier of K c= the InternalRel of K by RELAT_1:def 3;

now

let x, y be set ; :: thesis: ( [x,y] in the InternalRel of K implies [x,y] in the InternalRel of (SubstPoset V',C') |_2 the carrier of K )
assume A7: [x,y] in the InternalRel of K ; :: thesis: [x,y] in the InternalRel of (SubstPoset V',C') |_2 the carrier of K
then reconsider p = x, q = y as Element of by ZFMISC_1:106;
( x in the carrier of K & y in the carrier of K ) by A7, ZFMISC_1:106;
then reconsider p' = p, q' = q as Element of by A2;
p <= q by A7, ORDERS_2:def 9;
then for a being set st a in p holds
ex b being set st
( b in q & b c= a ) by Th15;
then p' <= q' by Th15;
then [p',q'] in the InternalRel of (SubstPoset V',C') by ORDERS_2:def 9;
hence [x,y] in the InternalRel of (SubstPoset V',C') |_2 the carrier of K by A7, XBOOLE_0:def 4; :: thesis: verum

end;

then the InternalRel of K c= the InternalRel of (SubstPoset V',C') |_2 the carrier of K by RELAT_1:def 3;
then the InternalRel of K = the InternalRel of (SubstPoset V',C') |_2 the carrier of K by A6, XBOOLE_0:def 10;
hence SubstPoset V,C is full SubRelStr of SubstPoset V',C' by YELLOW_0:def 14; :: thesis: verum