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) #) by WAYBEL_9:def 8;
A2: the mapping of (X opp+id) = (incl ((subrelstr X),R)) * the mapping of ((subrelstr X) opp+id) by WAYBEL_9:def 8;
A3: the carrier of (subrelstr X) = X by YELLOW_0:def 15;
A4: the carrier of ((subrelstr X) opp+id) = the carrier of (subrelstr X) by WAYBEL_9:def 6;
A5: the InternalRel of ((subrelstr X) opp+id) = the InternalRel of (subrelstr X) ~ by WAYBEL_9:def 6;
thus the carrier of (X opp+id) = X by A1, A3, 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 ) )
A6: 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 A3, YELLOW_0:def 14;
then A7: the InternalRel of ((subrelstr X) opp+id) = ( the InternalRel of R ~) |_2 X by A5, ORDERS_1:83;
then the InternalRel of ((subrelstr X) opp+id) c= the InternalRel of (R opp) by A6, XBOOLE_1:17;
then reconsider S = X opp+id as SubRelStr of R opp by A1, A3, A4, A6, YELLOW_0:def 13;
the InternalRel of S = the InternalRel of (R opp) |_2 the carrier of S by A1, A4, A6, A7, YELLOW_0:def 15;
hence X opp+id is full SubRelStr of R opp by YELLOW_0:def 14; :: 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 A8: the mapping of ((subrelstr X) opp+id) = id X by WAYBEL_9:def 6;
A9: dom (id X) = X ;
incl ((subrelstr X),R) = id X by A3, Def1;
then the mapping of (X opp+id) = id X by A2, A8, A9, RELAT_1:52;
hence (X opp+id) . x = x by A1, A3, A4; :: thesis: verum