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 )

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

thus ( L is reflexive implies L opp is reflexive ) :: thesis: ( L opp is reflexive implies L is reflexive )

proof

assume
L opp is reflexive
; :: thesis: L is reflexive
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;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

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