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