let R be Relation; :: thesis: ( R is empty implies ( R is reflexive & R is irreflexive & R is symmetric & R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive ) )
assume A1: R is empty ; :: thesis: ( R is reflexive & R is irreflexive & R is symmetric & R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive )
thus R is reflexive :: thesis: ( R is irreflexive & R is symmetric & R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive )

proof

let x be object ; :: according to RELAT_2:def 1,RELAT_2:def 9 :: thesis: ( x in field R implies [x,x] in R )
thus ( x in field R implies [x,x] in R ) by A1, RELAT_1:40; :: thesis: verum

end;

thus R is irreflexive :: thesis: ( R is symmetric & R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive )

proof

let x be object ; :: according to RELAT_2:def 2,RELAT_2:def 10 :: thesis: ( x in field R implies not [x,x] in R )
thus ( x in field R implies not [x,x] in R ) by A1; :: thesis: verum

end;

thus R is symmetric :: thesis: ( R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive )

proof

let x be object ; :: according to RELAT_2:def 3,RELAT_2:def 11 :: thesis: for y being object st x in field R & y in field R & [x,y] in R holds
[y,x] in R
thus for y being object st x in field R & y in field R & [x,y] in R holds
[y,x] in R by A1; :: thesis: verum

end;

thus R is antisymmetric :: thesis: ( R is asymmetric & R is connected & R is strongly_connected & R is transitive )

proof

let x be object ; :: according to RELAT_2:def 4,RELAT_2:def 12 :: thesis: for y being object st x in field R & y in field R & [x,y] in R & [y,x] in R holds
x = y
thus for y being object st x in field R & y in field R & [x,y] in R & [y,x] in R holds
x = y by A1; :: thesis: verum

end;

thus R is asymmetric :: thesis: ( R is connected & R is strongly_connected & R is transitive )

proof

let x be object ; :: according to RELAT_2:def 5,RELAT_2:def 13 :: thesis: for y being object st x in field R & y in field R & [x,y] in R holds
not [y,x] in R
thus for y being object st x in field R & y in field R & [x,y] in R holds
not [y,x] in R by A1; :: thesis: verum

end;

thus R is connected :: thesis: ( R is strongly_connected & R is transitive )

proof

let x be object ; :: according to RELAT_2:def 6,RELAT_2:def 14 :: thesis: for y being object st x in field R & y in field R & x <> y & not [x,y] in R holds
[y,x] in R
thus for y being object st x in field R & y in field R & x <> y & not [x,y] in R holds
[y,x] in R by A1, RELAT_1:40; :: thesis: verum

end;

thus R is strongly_connected :: thesis: R is transitive

proof

let x be object ; :: according to RELAT_2:def 7,RELAT_2:def 15 :: thesis: for y being object st x in field R & y in field R & not [x,y] in R holds
[y,x] in R
thus for y being object st x in field R & y in field R & not [x,y] in R holds
[y,x] in R by A1, RELAT_1:40; :: thesis: verum

end;

let x be object ; :: according to RELAT_2:def 8,RELAT_2:def 16 :: thesis: for y, z being object st x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R holds
[x,z] in R
thus for y, z being object st x in field R & y in field R & z in field R & [x,y] in R & [y,z] in R holds
[x,z] in R by A1; :: thesis: verum