let L be RelStr ; :: thesis: for x being Element of L
for y being Element of (L opp) holds
( ( x <= ~ y implies x ~ >= y ) & ( x ~ >= y implies x <= ~ y ) & ( x >= ~ y implies x ~ <= y ) & ( x ~ <= y implies x >= ~ y ) )
let x be Element of L; :: thesis: for y being Element of (L opp) holds
( ( x <= ~ y implies x ~ >= y ) & ( x ~ >= y implies x <= ~ y ) & ( x >= ~ y implies x ~ <= y ) & ( x ~ <= y implies x >= ~ y ) )
let y be Element of (L opp); :: thesis: ( ( x <= ~ y implies x ~ >= y ) & ( x ~ >= y implies x <= ~ y ) & ( x >= ~ y implies x ~ <= y ) & ( x ~ <= y implies x >= ~ y ) )
~ (x ~) = x ~ ;
hence ( ( x <= ~ y implies x ~ >= y ) & ( x ~ >= y implies x <= ~ y ) & ( x >= ~ y implies x ~ <= y ) & ( x ~ <= y implies x >= ~ y ) ) by Th1; :: thesis: verum