let R be non empty RelStr ; :: thesis: for X being non empty Subset of R holds
( the carrier of (X opp+id ) = X & X opp+id is full SubRelStr of R opp & ( for x being Element of (X opp+id ) holds (X opp+id ) . x = x ) )
let X be non empty Subset of R; :: thesis: ( the carrier of (X opp+id ) = X & X opp+id is full SubRelStr of R opp & ( for x being Element of (X opp+id ) holds (X opp+id ) . x = x ) )
A1: ( RelStr(# the carrier of (X opp+id ),the InternalRel of (X opp+id ) #) = RelStr(# the carrier of ((subrelstr X) opp+id ),the InternalRel of ((subrelstr X) opp+id ) #) & the mapping of (X opp+id ) = (incl (subrelstr X),R) * the mapping of ((subrelstr X) opp+id ) ) by WAYBEL_9:def 8;
A2: the carrier of (subrelstr X) = X by YELLOW_0:def 15;
A3: ( the carrier of ((subrelstr X) opp+id ) = the carrier of (subrelstr X) & RelStr(# the carrier of ((subrelstr X) opp+id ),the InternalRel of ((subrelstr X) opp+id ) #) = (subrelstr X) opp & the InternalRel of ((subrelstr X) opp+id ) = the InternalRel of (subrelstr X) ~ ) by WAYBEL_9:11, WAYBEL_9:def 6;
thus the carrier of (X opp+id ) = X by A1, A2, WAYBEL_9:def 6; :: thesis: ( X opp+id is full SubRelStr of R opp & ( for x being Element of (X opp+id ) holds (X opp+id ) . x = x ) )
A4: R opp = RelStr(# the carrier of R,(the InternalRel of R ~ ) #) by LATTICE3:def 5;
the InternalRel of (subrelstr X) = the InternalRel of R |_2 X by A2, YELLOW_0:def 14;
then A5: the InternalRel of ((subrelstr X) opp+id ) = (the InternalRel of R ~ ) |_2 X by A3, ORDERS_1:193;
then the InternalRel of ((subrelstr X) opp+id ) c= the InternalRel of (R opp ) by A4, XBOOLE_1:17;
then reconsider S = X opp+id as SubRelStr of R opp by A1, A2, A3, A4, YELLOW_0:def 13;
S is full

proof

thus the InternalRel of S = the InternalRel of (R opp ) |_2 the carrier of S by A1, A3, A4, A5, YELLOW_0:def 15; :: according to YELLOW_0:def 14 :: thesis: verum

end;

hence X opp+id is full SubRelStr of R opp ; :: thesis: for x being Element of (X opp+id ) holds (X opp+id ) . x = x
let x be Element of (X opp+id ); :: thesis: (X opp+id ) . x = x
id (subrelstr X) = id X by YELLOW_0:def 15;
then ( the mapping of ((subrelstr X) opp+id ) = id X & dom (id X) = X & incl (subrelstr X),R = id X ) by A2, Def1, RELAT_1:71, WAYBEL_9:def 6;
then the mapping of (X opp+id ) = id X by A1, RELAT_1:78;
hence (X opp+id ) . x = x by A1, A2, A3, FUNCT_1:35; :: thesis: verum