let L be RelStr ; :: thesis: for X being Subset of L holds RelStr(# X,( the InternalRel of L |_2 X) #) is full SubRelStr of L
let X be Subset of L; :: thesis: RelStr(# X,( the InternalRel of L |_2 X) #) is full SubRelStr of L
set S = RelStr(# X,( the InternalRel of L |_2 X) #);
the InternalRel of RelStr(# X,( the InternalRel of L |_2 X) #) c= the InternalRel of L by XBOOLE_1:17;
then reconsider S = RelStr(# X,( the InternalRel of L |_2 X) #) as SubRelStr of L by Def13;
S is full by Def14;
hence RelStr(# X,( the InternalRel of L |_2 X) #) is full SubRelStr of L ; :: thesis: verum