let x, y, c be non pair set ; :: thesis: ( x in InputVertices (BorrowStr x,y,c) & y in InputVertices (BorrowStr x,y,c) & c in InputVertices (BorrowStr x,y,c) )
A1: ( x in the carrier of (BorrowStr x,y,c) & y in the carrier of (BorrowStr x,y,c) & c in the carrier of (BorrowStr x,y,c) ) by Th6;
A2: InnerVertices (BorrowStr x,y,c) is Relation by Th1;
assume ( not x in InputVertices (BorrowStr x,y,c) or not y in InputVertices (BorrowStr x,y,c) or not c in InputVertices (BorrowStr x,y,c) ) ; :: thesis: contradiction
then ( x in InnerVertices (BorrowStr x,y,c) or y in InnerVertices (BorrowStr x,y,c) or c in InnerVertices (BorrowStr x,y,c) ) by A1, XBOOLE_0:def 5;
then ( ex a1, b1 being set st x = [a1,b1] or ex a1, b1 being set st y = [a1,b1] or ex a1, b1 being set st c = [a1,b1] ) by A2, RELAT_1:def 1;
hence contradiction ; :: thesis: verum