let A be antisymmetric RelStr ; :: thesis: for a1, a2 being Element of A st a1 <= a2 holds
not a2 < a1
let a1, a2 be Element of A; :: thesis: ( a1 <= a2 implies not a2 < a1 )
assume that
A1: a1 <= a2 and
A2: a2 < a1 ; :: thesis: contradiction
a2 <= a1 by A2, Def10;
hence contradiction by A1, A2, Th25; :: thesis: verum