defpred S₁[ set ] means ex y being Element of L st
( y = $1 & y is compact );
consider X being Subset of L such that
A1: for x being set holds
( x in X iff ( x in the carrier of L & S₁[x] ) ) from SUBSET_1:sch 1();
reconsider S = RelStr(# X,( the InternalRel of L |_2 X) #) as strict full SubRelStr of L by YELLOW_0:56;
take S ; :: thesis: for x being Element of L holds
( x in the carrier of S iff x is compact )
let x be Element of L; :: thesis: ( x in the carrier of S iff x is compact )
thus ( x in the carrier of S implies x is compact ) :: thesis: ( x is compact implies x in the carrier of S )

proof

assume x in the carrier of S ; :: thesis: x is compact
then ex y being Element of L st
( y = x & y is compact ) by A1;
hence x is compact ; :: thesis: verum

end;

thus ( x is compact implies x in the carrier of S ) by A1; :: thesis: verum