let x, y, c be non pair object ; :: 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 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 ; :: thesis: verum

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 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 ; :: thesis: verum