set T = { a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a2 < a1 } ;
{ a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a2 < a1 } c= the carrier of A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a2 < a1 } or x in the carrier of A )
assume x in { a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a2 < a1 } ; :: thesis: x in the carrier of A
then ex a1 being Element of A st
( x = a1 & ( for a2 being Element of A st a2 in S holds
a2 < a1 ) ) ;
hence x in the carrier of A ; :: thesis: verum

end;

hence { a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a2 < a1 } is Subset of A ; :: thesis: verum
thus verum ; :: thesis: verum