let G1, G2 be _Graph; :: thesis: ( G1 tolerates G2 iff {G1,G2} is \/-tolerating )
now :: thesis: ( G1 tolerates G2 implies for G3, G4 being Element of {G1,G2} holds G3 tolerates G4 )
assume A1: G1 tolerates G2 ; :: thesis: for G3, G4 being Element of {G1,G2} holds b3 tolerates b4
let G3, G4 be Element of {G1,G2}; :: thesis: b1 tolerates b2
per cases ( ( G3 = G1 & G4 = G1 ) or ( G3 = G1 & G4 = G2 ) or ( G3 = G2 & G4 = G1 ) or ( G3 = G2 & G4 = G2 ) ) by TARSKI:def 2;
suppose ( G3 = G1 & G4 = G1 ) ; :: thesis: b1 tolerates b2
hence G3 tolerates G4 ; :: thesis: verum
end;
suppose ( G3 = G1 & G4 = G2 ) ; :: thesis: b1 tolerates b2
hence G3 tolerates G4 by A1; :: thesis: verum
end;
suppose ( G3 = G2 & G4 = G1 ) ; :: thesis: b1 tolerates b2
hence G3 tolerates G4 by A1; :: thesis: verum
end;
suppose ( G3 = G2 & G4 = G2 ) ; :: thesis: b1 tolerates b2
hence G3 tolerates G4 ; :: thesis: verum
end;
end;
end;
hence ( G1 tolerates G2 implies {G1,G2} is \/-tolerating ) ; :: thesis: ( {G1,G2} is \/-tolerating implies G1 tolerates G2 )
assume A2: {G1,G2} is \/-tolerating ; :: thesis: G1 tolerates G2
( G1 in {G1,G2} & G2 in {G1,G2} ) by TARSKI:def 2;
hence G1 tolerates G2 by A2; :: thesis: verum