let S1, S2 be non empty 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 )
meet (the_Vertices_of (S1 \/ S2)) = meet ((the_Vertices_of S1) \/ (the_Vertices_of S2)) by Th8
.= (meet (the_Vertices_of S1)) /\ (meet (the_Vertices_of S2)) by SETFAM_1:9 ;
then A2: ( meet (the_Vertices_of S1) <> {} & meet (the_Vertices_of S2) <> {} ) by A1;
( S1 is \/-tolerating & S2 is \/-tolerating ) by A1, Th20;
hence ( S1 is /\-tolerating & S2 is /\-tolerating ) by A2; :: thesis: verum