let A be antisymmetric RelStr ; :: thesis: for a1, a2 being Element of A st a1 <= a2 & a2 <= a1 holds
a1 = a2
let a1, a2 be Element of A; :: thesis: ( a1 <= a2 & a2 <= a1 implies a1 = a2 )
assume that
A1: [a1,a2] in the InternalRel of A and
A2: [a2,a1] in the InternalRel of A ; :: according to ORDERS_2:def 5 :: thesis: a1 = a2
A3: the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
a1 in the carrier of A by A1, ZFMISC_1:87;
hence a1 = a2 by A1, A2, A3; :: thesis: verum