let T be reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure ; :: thesis: for t being type of T
for a being adjective of T
for A, B being Subset of the adjectives of T st B = A \/ {a} & B is_applicable_to t holds
a ast (A ast t) = B ast t
let t be type of T; :: thesis: for a being adjective of T
for A, B being Subset of the adjectives of T st B = A \/ {a} & B is_applicable_to t holds
a ast (A ast t) = B ast t
let a be adjective of T; :: thesis: for A, B being Subset of the adjectives of T st B = A \/ {a} & B is_applicable_to t holds
a ast (A ast t) = B ast t
let A, B be Subset of the adjectives of T; :: thesis: ( B = A \/ {a} & B is_applicable_to t implies a ast (A ast t) = B ast t )
assume that
A1: B = A \/ {a} and
A2: B is_applicable_to t ; :: thesis: a ast (A ast t) = B ast t
A3: A is_applicable_to t by A1, A2, Th54, XBOOLE_1:7;
A4: {a} c= B by A1, XBOOLE_1:7;
A5: A c= B by A1, XBOOLE_1:7;
(types a) /\ (downarrow (A ast t)) = (types B) /\ (downarrow t)

proof

thus (types a) /\ (downarrow (A ast t)) c= (types B) /\ (downarrow t) :: according to XBOOLE_0:def 10 :: thesis: (types B) /\ (downarrow t) c= (types a) /\ (downarrow (A ast t))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (types a) /\ (downarrow (A ast t)) or x in (types B) /\ (downarrow t) )
assume A6: x in (types a) /\ (downarrow (A ast t)) ; :: thesis: x in (types B) /\ (downarrow t)
then reconsider t9 = x as type of T ;
x in types a by A6, XBOOLE_0:def 4;
then a in adjs t9 by Th13;
then A7: {a} c= adjs t9 by ZFMISC_1:31;
x in downarrow (A ast t) by A6, XBOOLE_0:def 4;
then A8: t9 <= A ast t by WAYBEL_0:17;
then A9: adjs (A ast t) c= adjs t9 by Th10;
A ast t <= t by A3, Th49;
then t9 <= t by A8, YELLOW_0:def 2;
then A10: t9 in downarrow t by WAYBEL_0:17;
A c= adjs (A ast t) by A3, Th50;
then A c= adjs t9 by A9;
then B c= adjs t9 by A1, A7, XBOOLE_1:8;
then t9 in types B by Th14;
hence x in (types B) /\ (downarrow t) by A10, XBOOLE_0:def 4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (types B) /\ (downarrow t) or x in (types a) /\ (downarrow (A ast t)) )
assume A11: x in (types B) /\ (downarrow t) ; :: thesis: x in (types a) /\ (downarrow (A ast t))
then reconsider t9 = x as type of T ;
x in downarrow t by A11, XBOOLE_0:def 4;
then A12: t9 <= t by WAYBEL_0:17;
x in types B by A11, XBOOLE_0:def 4;
then A13: B c= adjs t9 by Th14;
then A c= adjs t9 by A5;
then t9 <= A ast t by A12, Th52;
then A14: t9 in downarrow (A ast t) by WAYBEL_0:17;
a in B by A4, ZFMISC_1:31;
then t9 in types a by A13, Th13;
hence x in (types a) /\ (downarrow (A ast t)) by A14, XBOOLE_0:def 4; :: thesis: verum

end;

hence a ast (A ast t) = B ast t ; :: thesis: verum