let X be set ; :: thesis: for R being reflexive connected total Relation of X
for R2 being Relation of X holds R \, R2 = R
let R be reflexive connected total Relation of X; :: thesis: for R2 being Relation of X holds R \, R2 = R
let R2 be Relation of X; :: thesis: R \, R2 = R
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in R \, R2 or [x,y] in R ) & ( not [x,y] in R or [x,y] in R \, R2 ) )
reconsider xx = x, yy = y as set by TARSKI:1;
hereby :: thesis: ( not [x,y] in R or [x,y] in R \, R2 )
assume [x,y] in R \, R2 ; :: thesis: [x,y] in R
then xx,yy in R \, R2 ;
then ( xx,yy in R or ( yy,xx nin R & xx,yy in R2 ) ) by Th9;
then ( [x,y] in R or ( [y,x] nin R & x in X & y in X & field R = X & R is_connected_in field R & R is_reflexive_in field R & ( x = y or x <> y ) ) ) by Th2, RELAT_2:def 9, RELAT_2:def 14, ORDERS_1:12;
hence [x,y] in R ; :: thesis: verum
end;
assume [x,y] in R ; :: thesis: [x,y] in R \, R2
then xx,yy in R ;
then xx,yy in R \, R2 by Th9;
hence [x,y] in R \, R2 ; :: thesis: verum