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)) )
assume A1: ( 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
A2: c in the carrier of (BorrowStr (x,y,c)) by Th6;
A3: InnerVertices (BorrowStr (x,y,c)) is Relation by Th1;
( x in the carrier of (BorrowStr (x,y,c)) & y in the carrier of (BorrowStr (x,y,c)) ) by Th6;
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 A2, A1, XBOOLE_0:def 5;
then ( ex a1, b1 being object st x = [a1,b1] or ex a1, b1 being object st y = [a1,b1] or ex a1, b1 being object st c = [a1,b1] ) by A3, RELAT_1:def 1;
hence contradiction ; :: thesis: verum