let S1, S2 be Graph-membered set ; :: thesis: ( S1 \/ S2 is \/-tolerating implies ( S1 is \/-tolerating & S2 is \/-tolerating ) )
assume A1: S1 \/ S2 is \/-tolerating ; :: thesis: ( S1 is \/-tolerating & S2 is \/-tolerating )
hereby :: according to GLIB_014:def 23 :: thesis: S2 is \/-tolerating
let G1, G2 be _Graph; :: thesis: ( G1 in S1 & G2 in S1 implies G1 tolerates G2 )
assume ( G1 in S1 & G2 in S1 ) ; :: thesis: G1 tolerates G2
then ( G1 in S1 \/ S2 & G2 in S1 \/ S2 ) by XBOOLE_0:def 3;
hence G1 tolerates G2 by A1; :: thesis: verum
end;
let G1, G2 be _Graph; :: according to GLIB_014:def 23 :: thesis: ( G1 in S2 & G2 in S2 implies G1 tolerates G2 )
assume ( G1 in S2 & G2 in S2 ) ; :: thesis: G1 tolerates G2
then ( G1 in S1 \/ S2 & G2 in S1 \/ S2 ) by XBOOLE_0:def 3;
hence G1 tolerates G2 by A1; :: thesis: verum