let A be RelStr ; :: thesis: for a, b being Element of A holds
( a <= b iff b ~ <= a ~ )
let a, b be Element of A; :: thesis: ( a <= b iff b ~ <= a ~ )
( RelStr(# the carrier of A,the InternalRel of A #) = RelStr(# the carrier of A,the InternalRel of A #) & A ~ = RelStr(# the carrier of A,(the InternalRel of A ~ ) #) & ( a <= b implies [a,b] in the InternalRel of A ) & ( [a,b] in the InternalRel of A implies a <= b ) & ( b ~ <= a ~ implies [(b ~ ),(a ~ )] in the InternalRel of (A ~ ) ) & ( [(b ~ ),(a ~ )] in the InternalRel of (A ~ ) implies b ~ <= a ~ ) & ( [a,b] in the InternalRel of A implies [b,a] in the InternalRel of A ~ ) & ( [b,a] in the InternalRel of A ~ implies [a,b] in the InternalRel of A ) & a = a ~ & b = b ~ ) by ORDERS_2:def 9, RELAT_1:def 7;
hence ( a <= b iff b ~ <= a ~ ) ; :: thesis: verum