let O be non empty connected Poset; :: thesis: for R being array of O holds inversions R c= [:(dom R),(dom R):]
let R be array of O; :: thesis: inversions R c= [:(dom R),(dom R):]
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in inversions R or x in [:(dom R),(dom R):] )
assume A1: x in inversions R ; :: thesis: x in [:(dom R),(dom R):]
then consider a, b being Element of dom R such that
A0: ( x = [a,b] & a in b & R /. a > R /. b ) ;
( a in dom R & b in dom R ) by A0, A1, TW0;
hence x in [:(dom R),(dom R):] by A0, ZFMISC_1:def 2; :: thesis: verum