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) #);
RelStr(# X,(the InternalRel of L |_2 X) #) is SubRelStr of L

proof

thus the carrier of RelStr(# X,(the InternalRel of L |_2 X) #) c= the carrier of L ; :: according to YELLOW_0:def 13 :: thesis: the InternalRel of RelStr(# X,(the InternalRel of L |_2 X) #) c= the InternalRel of L
thus the InternalRel of RelStr(# X,(the InternalRel of L |_2 X) #) c= the InternalRel of L by XBOOLE_1:17; :: thesis: verum

end;

then reconsider S = RelStr(# X,(the InternalRel of L |_2 X) #) as SubRelStr of L ;
S is full

proof

thus the InternalRel of S = the InternalRel of L |_2 the carrier of S ; :: according to YELLOW_0:def 14 :: thesis: verum

end;

hence RelStr(# X,(the InternalRel of L |_2 X) #) is full SubRelStr of L ; :: thesis: verum