let T be non empty reflexive transitive non void TAS-structure ; :: thesis: for t being type of T
for A being Subset of the adjectives of T st A is_properly_applicable_to t holds
ex B being Subset of the adjectives of T st
( B c= A & B is_properly_applicable_to t & A ast t = B ast t & ( for C being Subset of the adjectives of T st C c= B & C is_properly_applicable_to t & A ast t = C ast t holds
C = B ) )
let t be type of T; :: thesis: for A being Subset of the adjectives of T st A is_properly_applicable_to t holds
ex B being Subset of the adjectives of T st
( B c= A & B is_properly_applicable_to t & A ast t = B ast t & ( for C being Subset of the adjectives of T st C c= B & C is_properly_applicable_to t & A ast t = C ast t holds
C = B ) )
let A be Subset of the adjectives of T; :: thesis: ( A is_properly_applicable_to t implies ex B being Subset of the adjectives of T st
( B c= A & B is_properly_applicable_to t & A ast t = B ast t & ( for C being Subset of the adjectives of T st C c= B & C is_properly_applicable_to t & A ast t = C ast t holds
C = B ) ) )
defpred S₁[ set ] means ex B being Subset of the adjectives of T st
( $1 = B & $1 c= A & B is_properly_applicable_to t & A ast t = B ast t );
assume A is_properly_applicable_to t ; :: thesis: ex B being Subset of the adjectives of T st
( B c= A & B is_properly_applicable_to t & A ast t = B ast t & ( for C being Subset of the adjectives of T st C c= B & C is_properly_applicable_to t & A ast t = C ast t holds
C = B ) )
then ( A is finite & A c= A & A is_properly_applicable_to t & A ast t = A ast t ) by Th63;
then A1: ex a being finite set st S₁[a] ;
consider B being finite set such that
A2: S₁[B] and
A3: for C being set st C c= B & S₁[C] holds
C = B from ABCMIZ_0:sch 1(A1);
reconsider B = B as Subset of the adjectives of T by A2;
take B ; :: thesis: ( B c= A & B is_properly_applicable_to t & A ast t = B ast t & ( for C being Subset of the adjectives of T st C c= B & C is_properly_applicable_to t & A ast t = C ast t holds
C = B ) )
thus ( B c= A & B is_properly_applicable_to t & A ast t = B ast t ) by A2; :: thesis: for C being Subset of the adjectives of T st C c= B & C is_properly_applicable_to t & A ast t = C ast t holds
C = B
let C be Subset of the adjectives of T; :: thesis: ( C c= B & C is_properly_applicable_to t & A ast t = C ast t implies C = B )
assume A4: C c= B ; :: thesis: ( not C is_properly_applicable_to t or not A ast t = C ast t or C = B )
then C c= A by A2, XBOOLE_1:1;
hence ( not C is_properly_applicable_to t or not A ast t = C ast t or C = B ) by A3, A4; :: thesis: verum