thus ( 1 <> 2 & 1 <> 3 & 2 <> 3 ) ; :: according to ZFMISC_1:def 5 :: thesis: verum