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
proof
per cases ( R is empty or not R is empty ) ;
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;
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;
end;
end;
A5: R is_transitive_in field R
proof
per cases ( R is empty or not R is empty ) ;
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;
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;
end;
end;
A13: R is_strongly_connected_in field R
proof
per cases ( R is empty or not R is empty ) ;
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;
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;
end;
end;
R is_symmetric_in field R
proof
per cases ( R is empty or not R is empty ) ;
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;
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;
end;
end;
hence ( R is trivial & R is reflexive & R is symmetric & R is transitive & R is strongly_connected ) by A1, A5, A13; :: thesis: verum