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 )

[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

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

thus
R is irreflexive
:: thesis: ( R is symmetric & R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive )
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 ( x in field R implies [x,x] in R ) by A1, RELAT_1:40; :: thesis: verum

proof

thus
R is symmetric
:: thesis: ( R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive )
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 ( x in field R implies not [x,x] in R ) by A1; :: thesis: verum

proof

thus
R is antisymmetric
:: thesis: ( R is asymmetric & R is connected & R is strongly_connected & R is transitive )
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;[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

proof

thus
R is asymmetric
:: thesis: ( R is connected & R is strongly_connected & R is transitive )
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;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

proof

thus
R is connected
:: thesis: ( R is strongly_connected & R is transitive )
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;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

proof

thus
R is strongly_connected
:: thesis: R is transitive
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;[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

proof

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
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;[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

[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