set A = the non empty set ;
set r = the Relation of the non empty set ;
take X = ARS(# the non empty set , the Relation of the non empty set #); :: thesis: ( not X is empty & X is strict )
thus not X is empty ; :: thesis: X is strict
thus X is strict ; :: thesis: verum