let L be RelStr ; :: thesis: ( L is reflexive iff L opp is reflexive )
thus ( L is reflexive implies L opp is reflexive ) :: thesis: ( L opp is reflexive implies L is reflexive )

proof

assume L is reflexive ; :: thesis: L opp is reflexive
then A1: the InternalRel of L is_reflexive_in the carrier of L ;
let x be object ; :: according to RELAT_2:def 1,ORDERS_2:def 2 :: thesis: ( not x in the carrier of (L opp) or [x,x] in the InternalRel of (L opp) )
assume x in the carrier of (L opp) ; :: thesis: [x,x] in the InternalRel of (L opp)
then [x,x] in the InternalRel of L by A1;
hence [x,x] in the InternalRel of (L opp) by RELAT_1:def 7; :: thesis: verum

end;

assume L opp is reflexive ; :: thesis: L is reflexive
then A2: the InternalRel of (L opp) is_reflexive_in the carrier of (L opp) ;
let x be object ; :: according to RELAT_2:def 1,ORDERS_2:def 2 :: thesis: ( not x in the carrier of L or [x,x] in the InternalRel of L )
assume x in the carrier of L ; :: thesis: [x,x] in the InternalRel of L
then [x,x] in the InternalRel of (L opp) by A2;
hence [x,x] in the InternalRel of L by RELAT_1:def 7; :: thesis: verum