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;
A1: dom (id D) = D ;
rng (id D) = D ;
then reconsider g = id D as Function of D, the carrier of S by A1, FUNCT_2:def 1, RELSET_1:4;
(id the carrier of S) | D = id D by FUNCT_3:1;
then A2: 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 A2, YELLOW_0:def 13, YELLOW_0:def 14; :: thesis: verum