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 object ; :: 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
A2: ( x = [a,b] & a in b & R /. a > R /. b ) ;
( a in dom R & b in dom R ) by A2, A1, Th46;
hence x in [:(dom R),(dom R):] by A2, ZFMISC_1:def 2; :: thesis: verum