let K1, K2 be strict full SubRelStr of L; :: thesis: ( ( for x being Element of L holds
( x in the carrier of K1 iff x is compact ) ) & ( for x being Element of L holds
( x in the carrier of K2 iff x is compact ) ) implies K1 = K2 )
assume that
A3: for x being Element of L holds
( x in the carrier of K1 iff x is compact ) and
A4: for x being Element of L holds
( x in the carrier of K2 iff x is compact ) ; :: thesis: K1 = K2

now

let x be set ; :: thesis: ( ( x in the carrier of K1 implies x in the carrier of K2 ) & ( x in the carrier of K2 implies x in the carrier of K1 ) )
thus ( x in the carrier of K1 implies x in the carrier of K2 ) :: thesis: ( x in the carrier of K2 implies x in the carrier of K1 )

proof

A5: the carrier of K1 c= the carrier of L by YELLOW_0:def 13;
assume A6: x in the carrier of K1 ; :: thesis: x in the carrier of K2
then reconsider x' = x as Element of L by A5;
x' is compact by A3, A6;
hence x in the carrier of K2 by A4; :: thesis: verum

end;

thus ( x in the carrier of K2 implies x in the carrier of K1 ) :: thesis: verum

proof

A7: the carrier of K2 c= the carrier of L by YELLOW_0:def 13;
assume A8: x in the carrier of K2 ; :: thesis: x in the carrier of K1
then reconsider x' = x as Element of L by A7;
x' is compact by A4, A8;
hence x in the carrier of K1 by A3; :: thesis: verum

end;

end;

then the carrier of K1 = the carrier of K2 by TARSKI:2;
hence K1 = K2 by YELLOW_0:58; :: thesis: verum