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 b₃ tolerates b₄
let G3, G4 be Element of {G1,G2}; :: thesis: b₁ tolerates b₂

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: b₁ tolerates b₂

hence G3 tolerates G4 ; :: thesis: verum

end;

suppose ( G3 = G1 & G4 = G2 ) ; :: thesis: b₁ tolerates b₂

hence G3 tolerates G4 by A1; :: thesis: verum

end;

suppose ( G3 = G2 & G4 = G1 ) ; :: thesis: b₁ tolerates b₂

hence G3 tolerates G4 by A1; :: thesis: verum

end;

suppose ( G3 = G2 & G4 = G2 ) ; :: thesis: b₁ tolerates b₂

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