set Z = { y where y is Element of L : ( x >= y & y is compact ) } ;
defpred S1[ Element of L] means ( x >= $1 & $1 is compact );
consider X being Subset of L such that
A1: for y being Element of L holds
( y in X iff S1[y] ) from SUBSET_1:sch 3();
now :: thesis: for z being object holds
( ( z in X implies z in { y where y is Element of L : ( x >= y & y is compact ) } ) & ( z in { y where y is Element of L : ( x >= y & y is compact ) } implies z in X ) )
let z be object ; :: thesis: ( ( z in X implies z in { y where y is Element of L : ( x >= y & y is compact ) } ) & ( z in { y where y is Element of L : ( x >= y & y is compact ) } implies z in X ) )
thus ( z in X implies z in { y where y is Element of L : ( x >= y & y is compact ) } ) :: thesis: ( z in { y where y is Element of L : ( x >= y & y is compact ) } implies z in X )
proof
assume A2: z in X ; :: thesis: z in { y where y is Element of L : ( x >= y & y is compact ) }
then reconsider z1 = z as Element of L ;
( x >= z1 & z1 is compact ) by A1, A2;
hence z in { y where y is Element of L : ( x >= y & y is compact ) } ; :: thesis: verum
end;
thus ( z in { y where y is Element of L : ( x >= y & y is compact ) } implies z in X ) :: thesis: verum
proof
assume z in { y where y is Element of L : ( x >= y & y is compact ) } ; :: thesis: z in X
then ex v being Element of L st
( v = z & x >= v & v is compact ) ;
hence z in X by A1; :: thesis: verum
end;
end;
hence { y where y is Element of L : ( x >= y & y is compact ) } is Subset of L by TARSKI:2; :: thesis: verum