set w = the Element of inversions A;
assume not inversions A is empty ; :: thesis: contradiction
then the Element of inversions A in inversions A ;
then consider a, b being Element of dom A such that
A1: ( the Element of inversions A = [a,b] & a in b & not A /. a <= A /. b ) ;
thus contradiction by A1, SUBSET_1:def 1; :: thesis: verum