set H = { x where x is Element of C : F . x >= alpha } ;
{ x where x is Element of C : F . x >= alpha } c= C

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of C : F . x >= alpha } or y in C )
assume y in { x where x is Element of C : F . x >= alpha } ; :: thesis: y in C
then consider x being Element of C such that
A1: ( y = x & F . x >= alpha ) ;
thus y in C by A1; :: thesis: verum

end;

hence { x where x is Element of C : F . x >= alpha } is Subset of C ; :: thesis: verum