let R be non empty RelStr ; 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; ( 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; ( 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; for x being Element of (X opp+id) holds (X opp+id) . x = x
let x be Element of (X opp+id); (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
by RELAT_1:45;
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, FUNCT_1:18; verum