let x1, x2 be set ; :: according to RELAT_2:def 7,ORDERS_2:def 11 :: thesis: ( not x1 in {} A or not x2 in {} A or [x1,x2] in the InternalRel of A or [x2,x1] in the InternalRel of A )
thus ( not x1 in {} A or not x2 in {} A or [x1,x2] in the InternalRel of A or [x2,x1] in the InternalRel of A ) ; :: thesis: verum