let a, b, c be Ordinal; :: thesis: a in Tarski-Class ((a \/ b) \/ c)
set U = Tarski-Class ((a \/ b) \/ c);
( a c= a \/ b & a \/ b c= (a \/ b) \/ c ) by XBOOLE_1:7;
then ( a c= (a \/ b) \/ c & (a \/ b) \/ c in Tarski-Class ((a \/ b) \/ c) ) by CLASSES1:2;
hence a in Tarski-Class ((a \/ b) \/ c) by CLASSES1:def 1; :: thesis: verum