let S be non empty reflexive RelStr ; :: thesis: for D being non empty Subset of S holds
( the mapping of (Net-Str D) = id D & the carrier of (Net-Str D) = D & Net-Str D is full SubRelStr of S )
let D be non empty Subset of S; :: thesis: ( the mapping of (Net-Str D) = id D & the carrier of (Net-Str D) = D & Net-Str D is full SubRelStr of S )
set N = Net-Str D;
( dom (id D) = D & rng (id D) = D ) by RELAT_1:71;
then reconsider g = id D as Function of D,the carrier of S by FUNCT_2:def 1, RELSET_1:11;
(id the carrier of S) | D = id D by FUNCT_3:1;
then A1: Net-Str D = NetStr(# D,(the InternalRel of S |_2 D),g #) by WAYBEL17:def 4;
then the InternalRel of (Net-Str D) c= the InternalRel of S by XBOOLE_1:17;
hence ( the mapping of (Net-Str D) = id D & the carrier of (Net-Str D) = D & Net-Str D is full SubRelStr of S ) by A1, YELLOW_0:def 13, YELLOW_0:def 14; :: thesis: verum