let L be RelStr ; :: thesis: for x being Element of
for y being Element of 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 ; :: thesis: for y being Element of 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 ; :: 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