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 that
A1: a1 < a2 and
A2: a2 < a1 ; :: thesis: contradiction
( a1 <= a2 & a2 <= a1 ) by A1, A2, Def10;
hence contradiction by A1, Th25; :: thesis: verum