let A be antisymmetric RelStr ; :: thesis: for a1, a2 being Element of A holds
( not a1 < a2 or not a2 < a1 )
let a1, a2 be Element of A; :: thesis: ( not a1 < a2 or not a2 < a1 )
assume ( a1 < a2 & a2 < a1 ) ; :: thesis: contradiction
then ( a1 <= a2 & a1 <> a2 & a2 <= a1 ) by Def10;
hence contradiction by Th25; :: thesis: verum