let x, y, c be non pair object ; ( 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)) )
; 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 object st x = [a,b] or ex a, b being object st y = [a,b] or ex a, b being object st c = [a,b] )
by A3, RELAT_1:def 1;
hence
contradiction
; verum