set T = { a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a1 < a2 } ;
{ a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a1 < a2 } 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
a1 < a2 } 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
a1 < a2 } ; :: 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
a1 < a2 ) ) ;
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
a1 < a2 } is Subset of A ; :: thesis: verum
thus verum ; :: thesis: verum