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 ~ )
A1: ( a <= b iff [a,b] in the InternalRel of A ) by ORDERS_2:def 5;
( b ~ <= a ~ iff [(b ~),(a ~)] in the InternalRel of (A ~) ) by ORDERS_2:def 5;
hence ( a <= b iff b ~ <= a ~ ) by A1, RELAT_1:def 7; :: thesis: verum