let R be Relation; :: thesis: ( R is connected iff [:(field R),(field R):] = (R \/ (R ~)) \/ (id (field R)) )

hereby :: thesis: ( [:(field R),(field R):] = (R \/ (R ~)) \/ (id (field R)) implies R is connected )

assume R is connected ; :: thesis: [:(field R),(field R):] = (R \/ (R ~)) \/ (id (field R))
then [:(field R),(field R):] \ (id (field R)) c= R \/ (R ~) by RELAT_2:28;
then Z0: [:(field R),(field R):] c= (R \/ (R ~)) \/ (id (field R)) by XBOOLE_1:44;
C1: R c= [:(dom R),(rng R):] by RELAT_1:7;
( dom (R ~) = rng R & rng (R ~) = dom R ) by RELAT_1:20;
then C2: R ~ c= [:(rng R),(dom R):] by RELAT_1:7;
set GG = [:(rng R),(rng R):] \/ [:(dom R),(dom R):];
set D = [:(dom R),(dom R):];
set RR = [:(rng R),(rng R):];
set DR = [:(dom R),(rng R):];
set RI = (R \/ (R ~)) \/ (id (field R));
R \/ (R ~) c= [:(dom R),(rng R):] \/ [:(rng R),(dom R):] by XBOOLE_1:13, C1, C2;
then C4: (R \/ (R ~)) \/ (id (field R)) c= ([:(dom R),(rng R):] \/ [:(rng R),(dom R):]) \/ [:(field R),(field R):] by XBOOLE_1:13;
Z1: [:(field R),(field R):] = (([:(dom R),(dom R):] \/ [:(dom R),(rng R):]) \/ [:(rng R),(dom R):]) \/ [:(rng R),(rng R):] by ZFMISC_1:98;
then (R \/ (R ~)) \/ (id (field R)) c= ([:(dom R),(rng R):] \/ [:(rng R),(dom R):]) \/ (([:(dom R),(rng R):] \/ [:(dom R),(dom R):]) \/ ([:(rng R),(dom R):] \/ [:(rng R),(rng R):])) by C4, XBOOLE_1:4;
then (R \/ (R ~)) \/ (id (field R)) c= [:(rng R),(dom R):] \/ ([:(dom R),(rng R):] \/ (([:(dom R),(rng R):] \/ [:(dom R),(dom R):]) \/ ([:(rng R),(dom R):] \/ [:(rng R),(rng R):]))) by XBOOLE_1:4;
then (R \/ (R ~)) \/ (id (field R)) c= [:(rng R),(dom R):] \/ ([:(dom R),(rng R):] \/ ([:(dom R),(rng R):] \/ ([:(dom R),(dom R):] \/ ([:(rng R),(dom R):] \/ [:(rng R),(rng R):])))) by XBOOLE_1:4;
then (R \/ (R ~)) \/ (id (field R)) c= [:(rng R),(dom R):] \/ (([:(dom R),(rng R):] \/ [:(dom R),(rng R):]) \/ ([:(dom R),(dom R):] \/ ([:(rng R),(dom R):] \/ [:(rng R),(rng R):]))) by XBOOLE_1:4;
then (R \/ (R ~)) \/ (id (field R)) c= [:(rng R),(dom R):] \/ (([:(rng R),(dom R):] \/ ([:(rng R),(rng R):] \/ [:(dom R),(dom R):])) \/ [:(dom R),(rng R):]) by XBOOLE_1:4;
then (R \/ (R ~)) \/ (id (field R)) c= [:(rng R),(dom R):] \/ ([:(rng R),(dom R):] \/ (([:(rng R),(rng R):] \/ [:(dom R),(dom R):]) \/ [:(dom R),(rng R):])) by XBOOLE_1:4;
then (R \/ (R ~)) \/ (id (field R)) c= ([:(rng R),(dom R):] \/ [:(rng R),(dom R):]) \/ (([:(rng R),(rng R):] \/ [:(dom R),(dom R):]) \/ [:(dom R),(rng R):]) by XBOOLE_1:4;
then (R \/ (R ~)) \/ (id (field R)) c= ([:(rng R),(rng R):] \/ [:(dom R),(dom R):]) \/ ([:(dom R),(rng R):] \/ [:(rng R),(dom R):]) by XBOOLE_1:4;
then (R \/ (R ~)) \/ (id (field R)) c= ([:(dom R),(dom R):] \/ ([:(dom R),(rng R):] \/ [:(rng R),(dom R):])) \/ [:(rng R),(rng R):] by XBOOLE_1:4;
then (R \/ (R ~)) \/ (id (field R)) c= [:(field R),(field R):] by Z1, XBOOLE_1:4;
hence [:(field R),(field R):] = (R \/ (R ~)) \/ (id (field R)) by Z0, XBOOLE_0:def 10; :: thesis: verum

end;

assume [:(field R),(field R):] = (R \/ (R ~)) \/ (id (field R)) ; :: thesis: R is connected
then [:(field R),(field R):] \ (id (field R)) c= (R \/ (R ~)) \ (id (field R)) by XBOOLE_1:40;
hence R is connected by RELAT_2:28, XBOOLE_1:1; :: thesis: verum