set X = {0};
set r = {} [:{0},{0}:];
take R = RelStr(# {0},({} [:{0},{0}:]) #); :: thesis: ( R is asymmetric & R is transitive & not R is empty )
thus R is asymmetric :: thesis: ( R is transitive & not R is empty )
proof
let a be object ; :: according to RELAT_2:def 5,OPOSET_1:def 9 :: thesis: for b1 being object holds
( not a in the carrier of R or not b1 in the carrier of R or not [a,b1] in the InternalRel of R or not [b1,a] in the InternalRel of R )
let b be object ; :: thesis: ( not a in the carrier of R or not b in the carrier of R or not [a,b] in the InternalRel of R or not [b,a] in the InternalRel of R )
assume ( a in the carrier of R & b in the carrier of R ) ; :: thesis: ( not [a,b] in the InternalRel of R or not [b,a] in the InternalRel of R )
thus ( not [a,b] in the InternalRel of R or not [b,a] in the InternalRel of R ) ; :: thesis: verum
end;
thus R is transitive :: thesis: not R is empty
proof
let a be object ; :: according to RELAT_2:def 8,ORDERS_2:def 3 :: thesis: for b1, b2 being object holds
( not a in the carrier of R or not b1 in the carrier of R or not b2 in the carrier of R or not [a,b1] in the InternalRel of R or not [b1,b2] in the InternalRel of R or [a,b2] in the InternalRel of R )
thus for b1, b2 being object holds
( not a in the carrier of R or not b1 in the carrier of R or not b2 in the carrier of R or not [a,b1] in the InternalRel of R or not [b1,b2] in the InternalRel of R or [a,b2] in the InternalRel of R ) ; :: thesis: verum
end;
thus not R is empty ; :: thesis: verum