let G1, G2 be Graph; :: thesis: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 implies (bool G1) \/ (bool G2) c= bool (G1 \/ G2) )
assume A1: ( the Source of G1 tolerates the Source of G2 & the Target of G1 tolerates the Target of G2 ) ; :: thesis: (bool G1) \/ (bool G2) c= bool (G1 \/ G2)
A2: for v being set st v in bool G1 holds
v in bool (G1 \/ G2)
proof
let v be set ; :: thesis: ( v in bool G1 implies v in bool (G1 \/ G2) )
assume v in bool G1 ; :: thesis: v in bool (G1 \/ G2)
then reconsider G = v as strict Subgraph of G1 by Def25;
( G c= G1 & G1 c= G1 \/ G2 ) by A1, Th19;
then G c= G1 \/ G2 by Th17;
then G is strict Subgraph of G1 \/ G2 ;
hence v in bool (G1 \/ G2) by Def25; :: thesis: verum
end;
A3: for v being set st v in bool G2 holds
v in bool (G1 \/ G2)
proof
let v be set ; :: thesis: ( v in bool G2 implies v in bool (G1 \/ G2) )
assume v in bool G2 ; :: thesis: v in bool (G1 \/ G2)
then reconsider G = v as strict Subgraph of G2 by Def25;
( G c= G2 & G2 c= G1 \/ G2 ) by A1, Th19;
then G c= G1 \/ G2 by Th17;
then G is strict Subgraph of G1 \/ G2 ;
hence v in bool (G1 \/ G2) by Def25; :: thesis: verum
end;
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in (bool G1) \/ (bool G2) or v in bool (G1 \/ G2) )
assume v in (bool G1) \/ (bool G2) ; :: thesis: v in bool (G1 \/ G2)
then ( v in bool G1 or v in bool G2 ) by XBOOLE_0:def 3;
hence v in bool (G1 \/ G2) by A2, A3; :: thesis: verum