let L be RelStr ; :: thesis: for x being Element of (L opp)
for X being set holds
( ( x is_<=_than X implies ~ x is_>=_than X ) & ( ~ x is_>=_than X implies x is_<=_than X ) & ( x is_>=_than X implies ~ x is_<=_than X ) & ( ~ x is_<=_than X implies x is_>=_than X ) )
let x be Element of (L opp); :: thesis: for X being set holds
( ( x is_<=_than X implies ~ x is_>=_than X ) & ( ~ x is_>=_than X implies x is_<=_than X ) & ( x is_>=_than X implies ~ x is_<=_than X ) & ( ~ x is_<=_than X implies x is_>=_than X ) )
let X be set ; :: thesis: ( ( x is_<=_than X implies ~ x is_>=_than X ) & ( ~ x is_>=_than X implies x is_<=_than X ) & ( x is_>=_than X implies ~ x is_<=_than X ) & ( ~ x is_<=_than X implies x is_>=_than X ) )
(~ x) ~ = ~ x ;
hence ( ( x is_<=_than X implies ~ x is_>=_than X ) & ( ~ x is_>=_than X implies x is_<=_than X ) & ( x is_>=_than X implies ~ x is_<=_than X ) & ( ~ x is_<=_than X implies x is_>=_than X ) ) by Th8; :: thesis: verum