let R be non empty RelStr ; :: thesis: for X being non empty Subset of R holds
( the carrier of (X +id ) = X & X +id is full SubRelStr of R & ( for x being Element of (X +id ) holds (X +id ) . x = x ) )
let X be non empty Subset of R; :: thesis: ( the carrier of (X +id ) = X & X +id is full SubRelStr of R & ( for x being Element of (X +id ) holds (X +id ) . x = x ) )
A1: RelStr(# the carrier of (X +id ),the InternalRel of (X +id ) #) = RelStr(# the carrier of ((subrelstr X) +id ),the InternalRel of ((subrelstr X) +id ) #) by WAYBEL_9:def 8;
A2: the mapping of (X +id ) = (incl (subrelstr X),R) * the mapping of ((subrelstr X) +id ) by WAYBEL_9:def 8;
A3: the carrier of (subrelstr X) = X by YELLOW_0:def 15;
hence A4: the carrier of (X +id ) = X by A1, WAYBEL_9:def 5; :: thesis: ( X +id is full SubRelStr of R & ( for x being Element of (X +id ) holds (X +id ) . x = x ) )
A5: RelStr(# the carrier of ((subrelstr X) +id ),the InternalRel of ((subrelstr X) +id ) #) = subrelstr X by WAYBEL_9:def 5;
the InternalRel of (subrelstr X) c= the InternalRel of R by YELLOW_0:def 13;
then reconsider S = X +id as SubRelStr of R by A1, A3, A5, YELLOW_0:def 13;
the InternalRel of S = the InternalRel of R |_2 the carrier of S by A1, A5, YELLOW_0:def 14;
hence X +id is full SubRelStr of R by YELLOW_0:def 14; :: thesis: for x being Element of (X +id ) holds (X +id ) . x = x
let x be Element of (X +id ); :: thesis: (X +id ) . x = x
id (subrelstr X) = id X by YELLOW_0:def 15;
then A6: the mapping of ((subrelstr X) +id ) = id X by WAYBEL_9:def 5;
A7: dom (id X) = X by RELAT_1:71;
incl (subrelstr X),R = id X by A3, Def1;
then the mapping of (X +id ) = id X by A2, A6, A7, RELAT_1:78;
hence (X +id ) . x = x by A4, FUNCT_1:35; :: thesis: verum