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 )
for x being set st x in {} holds
[x,x] in {} ;
then {} is_reflexive_in field {} by RELAT_2:def 1;
hence R is reflexive by A1, RELAT_2:def 9; :: thesis: ( R is irreflexive & R is symmetric & R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive )
{} is_irreflexive_in field {}

proof

let x be set ; :: according to RELAT_2:def 2 :: thesis: ( not x in field {} or not [x,x] in {} )
assume x in field {} ; :: thesis: not [x,x] in {}
thus not [x,x] in {} ; :: thesis: verum

end;

hence R is irreflexive by A1, RELAT_2:def 10; :: thesis: ( R is symmetric & R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive )
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 set ; :: according to RELAT_2:def 3,RELAT_2:def 11 :: thesis: for b₁ being set holds
( not x in field R or not b₁ in field R or not [x,b₁] in R or [b₁,x] in R )
let y be set ; :: thesis: ( not x in field R or not y in field R or not [x,y] in R or [y,x] in R )
assume that
x in field R and
y in field R and
A2: [x,y] in R ; :: thesis: [y,x] in R
thus [y,x] in R by A1, A2; :: thesis: verum

end;

{} is_antisymmetric_in field {}

proof

let x be set ; :: according to RELAT_2:def 4 :: thesis: for b₁ being set holds
( not x in field {} or not b₁ in field {} or not [x,b₁] in {} or not [b₁,x] in {} or x = b₁ )
let y be set ; :: thesis: ( not x in field {} or not y in field {} or not [x,y] in {} or not [y,x] in {} or x = y )
assume that
A3: x in field {} and
y in field {} and
[x,y] in {} and
[y,x] in {} ; :: thesis: x = y
thus x = y by A3; :: thesis: verum

end;

hence R is antisymmetric by A1, RELAT_2:def 12; :: thesis: ( R is asymmetric & R is connected & R is strongly_connected & R is transitive )
{} is_asymmetric_in field {}

proof

let x be set ; :: according to RELAT_2:def 5 :: thesis: for b₁ being set holds
( not x in field {} or not b₁ in field {} or not [x,b₁] in {} or not [b₁,x] in {} )
let y be set ; :: thesis: ( not x in field {} or not y in field {} or not [x,y] in {} or not [y,x] in {} )
assume that
x in field {} and
y in field {} and
[x,y] in {} ; :: thesis: not [y,x] in {}
thus not [y,x] in {} ; :: thesis: verum

end;

hence R is asymmetric by A1, RELAT_2:def 13; :: thesis: ( R is connected & R is strongly_connected & R is transitive )
{} is_connected_in field {}

proof

let x be set ; :: according to RELAT_2:def 6 :: thesis: for b₁ being set holds
( not x in field {} or not b₁ in field {} or x = b₁ or [x,b₁] in {} or [b₁,x] in {} )
let y be set ; :: thesis: ( not x in field {} or not y in field {} or x = y or [x,y] in {} or [y,x] in {} )
assume that
A4: x in field {} and
y in field {} and
x <> y ; :: thesis: ( [x,y] in {} or [y,x] in {} )
thus ( [x,y] in {} or [y,x] in {} ) by A4; :: thesis: verum

end;

hence R is connected by A1, RELAT_2:def 14; :: thesis: ( R is strongly_connected & R is transitive )
{} is_strongly_connected_in field {}

proof

let x be set ; :: according to RELAT_2:def 7 :: thesis: for b₁ being set holds
( not x in field {} or not b₁ in field {} or [x,b₁] in {} or [b₁,x] in {} )
let y be set ; :: thesis: ( not x in field {} or not y in field {} or [x,y] in {} or [y,x] in {} )
assume that
A5: x in field {} and
y in field {} ; :: thesis: ( [x,y] in {} or [y,x] in {} )
thus ( [x,y] in {} or [y,x] in {} ) by A5; :: thesis: verum

end;

hence R is strongly_connected by A1, RELAT_2:def 15; :: thesis: R is transitive
{} is_transitive_in field {}

proof

let x be set ; :: according to RELAT_2:def 8 :: thesis: for b₁, b₂ being set holds
( not x in field {} or not b₁ in field {} or not b₂ in field {} or not [x,b₁] in {} or not [b₁,b₂] in {} or [x,b₂] in {} )
let y, z be set ; :: thesis: ( not x in field {} or not y in field {} or not z in field {} or not [x,y] in {} or not [y,z] in {} or [x,z] in {} )
assume that
A6: x in field {} and
y in field {} and
z in field {} and
[x,y] in {} and
[y,z] in {} ; :: thesis: [x,z] in {}
thus [x,z] in {} by A6; :: thesis: verum

end;

hence R is transitive by A1, RELAT_2:def 16; :: thesis: verum