let R be Relation of X,X; :: thesis: ( R is trivial & R is reflexive & R is symmetric & R is transitive & R is strongly_connected )

A1: R is_reflexive_in field R

A1: R is_reflexive_in field R

proof
end;

A5:
R is_transitive_in field R
per cases
( R is empty or not R is empty )
;

end;

suppose A2:
R is empty
; :: thesis: R is_reflexive_in field R

let x be object ; :: according to RELAT_2:def 1 :: thesis: ( not x in field R or [x,x] in R )

assume x in field R ; :: thesis: [x,x] in R

hence [x,x] in R by A2, RELAT_1:40; :: thesis: verum

end;assume x in field R ; :: thesis: [x,x] in R

hence [x,x] in R by A2, RELAT_1:40; :: thesis: verum

suppose
not R is empty
; :: thesis: R is_reflexive_in field R

then consider z being object such that

A3: R = {[z,z]} by Th4;

let x be object ; :: according to RELAT_2:def 1 :: thesis: ( not x in field R or [x,x] in R )

assume x in field R ; :: thesis: [x,x] in R

then A4: x in (dom R) \/ (rng R) by RELAT_1:def 6;

( dom R = {z} & rng R = {z} ) by A3, RELAT_1:9;

then x = z by A4, TARSKI:def 1;

hence [x,x] in R by A3, TARSKI:def 1; :: thesis: verum

end;A3: R = {[z,z]} by Th4;

let x be object ; :: according to RELAT_2:def 1 :: thesis: ( not x in field R or [x,x] in R )

assume x in field R ; :: thesis: [x,x] in R

then A4: x in (dom R) \/ (rng R) by RELAT_1:def 6;

( dom R = {z} & rng R = {z} ) by A3, RELAT_1:9;

then x = z by A4, TARSKI:def 1;

hence [x,x] in R by A3, TARSKI:def 1; :: thesis: verum

proof
end;

A13:
R is_strongly_connected_in field R
per cases
( R is empty or not R is empty )
;

end;

suppose A6:
R is empty
; :: thesis: R is_transitive_in field R

let x, y, z be object ; :: according to RELAT_2:def 8 :: thesis: ( not x in field R or not y in field R or not z in field R or not [x,y] in R or not [y,z] in R or [x,z] in R )

assume that

x in field R and

y in field R and

z in field R and

A7: [x,y] in R and

[y,z] in R ; :: thesis: [x,z] in R

thus [x,z] in R by A6, A7; :: thesis: verum

end;assume that

x in field R and

y in field R and

z in field R and

A7: [x,y] in R and

[y,z] in R ; :: thesis: [x,z] in R

thus [x,z] in R by A6, A7; :: thesis: verum

suppose A8:
not R is empty
; :: thesis: R is_transitive_in field R

let x, y, z be object ; :: according to RELAT_2:def 8 :: thesis: ( not x in field R or not y in field R or not z in field R or not [x,y] in R or not [y,z] in R or [x,z] in R )

assume that

x in field R and

y in field R and

z in field R and

A9: [x,y] in R and

A10: [y,z] in R ; :: thesis: [x,z] in R

consider a being object such that

A11: R = {[a,a]} by A8, Th4;

[y,z] = [a,a] by A11, A10, TARSKI:def 1;

then A12: z = a by XTUPLE_0:1;

[x,y] = [a,a] by A11, A9, TARSKI:def 1;

then x = a by XTUPLE_0:1;

hence [x,z] in R by A11, A12, TARSKI:def 1; :: thesis: verum

end;assume that

x in field R and

y in field R and

z in field R and

A9: [x,y] in R and

A10: [y,z] in R ; :: thesis: [x,z] in R

consider a being object such that

A11: R = {[a,a]} by A8, Th4;

[y,z] = [a,a] by A11, A10, TARSKI:def 1;

then A12: z = a by XTUPLE_0:1;

[x,y] = [a,a] by A11, A9, TARSKI:def 1;

then x = a by XTUPLE_0:1;

hence [x,z] in R by A11, A12, TARSKI:def 1; :: thesis: verum

proof
end;

R is_symmetric_in field R
per cases
( R is empty or not R is empty )
;

end;

suppose A14:
R is empty
; :: thesis: R is_strongly_connected_in field R

let x, y be object ; :: according to RELAT_2:def 7 :: thesis: ( not x in field R or not y in field R or [x,y] in R or [y,x] in R )

assume that

A15: x in field R and

y in field R ; :: thesis: ( [x,y] in R or [y,x] in R )

thus ( [x,y] in R or [y,x] in R ) by A14, A15, RELAT_1:40; :: thesis: verum

end;assume that

A15: x in field R and

y in field R ; :: thesis: ( [x,y] in R or [y,x] in R )

thus ( [x,y] in R or [y,x] in R ) by A14, A15, RELAT_1:40; :: thesis: verum

suppose A16:
not R is empty
; :: thesis: R is_strongly_connected_in field R

let x, y be object ; :: according to RELAT_2:def 7 :: thesis: ( not x in field R or not y in field R or [x,y] in R or [y,x] in R )

assume that

A17: x in field R and

A18: y in field R ; :: thesis: ( [x,y] in R or [y,x] in R )

consider a being object such that

A19: R = {[a,a]} by A16, Th4;

A20: ( dom R = {a} & rng R = {a} ) by A19, RELAT_1:9;

y in (dom R) \/ (rng R) by A18, RELAT_1:def 6;

then A21: y = a by A20, TARSKI:def 1;

x in (dom R) \/ (rng R) by A17, RELAT_1:def 6;

then x = a by A20, TARSKI:def 1;

hence ( [x,y] in R or [y,x] in R ) by A19, A21, TARSKI:def 1; :: thesis: verum

end;assume that

A17: x in field R and

A18: y in field R ; :: thesis: ( [x,y] in R or [y,x] in R )

consider a being object such that

A19: R = {[a,a]} by A16, Th4;

A20: ( dom R = {a} & rng R = {a} ) by A19, RELAT_1:9;

y in (dom R) \/ (rng R) by A18, RELAT_1:def 6;

then A21: y = a by A20, TARSKI:def 1;

x in (dom R) \/ (rng R) by A17, RELAT_1:def 6;

then x = a by A20, TARSKI:def 1;

hence ( [x,y] in R or [y,x] in R ) by A19, A21, TARSKI:def 1; :: thesis: verum

proof
end;

hence
( R is trivial & R is reflexive & R is symmetric & R is transitive & R is strongly_connected )
by A1, A5, A13; :: thesis: verumper cases
( R is empty or not R is empty )
;

end;

suppose A22:
R is empty
; :: thesis: R is_symmetric_in field R

let x, y be object ; :: according to RELAT_2:def 3 :: 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

A23: [x,y] in R ; :: thesis: [y,x] in R

thus [y,x] in R by A22, A23; :: thesis: verum

end;assume that

x in field R and

y in field R and

A23: [x,y] in R ; :: thesis: [y,x] in R

thus [y,x] in R by A22, A23; :: thesis: verum

suppose A24:
not R is empty
; :: thesis: R is_symmetric_in field R

let x, y be object ; :: according to RELAT_2:def 3 :: 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

A25: [x,y] in R ; :: thesis: [y,x] in R

consider a being object such that

A26: R = {[a,a]} by A24, Th4;

[x,y] = [a,a] by A26, A25, TARSKI:def 1;

then ( x = a & y = a ) by XTUPLE_0:1;

hence [y,x] in R by A26, TARSKI:def 1; :: thesis: verum

end;assume that

x in field R and

y in field R and

A25: [x,y] in R ; :: thesis: [y,x] in R

consider a being object such that

A26: R = {[a,a]} by A24, Th4;

[x,y] = [a,a] by A26, A25, TARSKI:def 1;

then ( x = a & y = a ) by XTUPLE_0:1;

hence [y,x] in R by A26, TARSKI:def 1; :: thesis: verum