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
A2: for x being Element of L holds
( x in the carrier of K1 iff x is compact ) and
A3: for x being Element of L holds
( x in the carrier of K2 iff x is compact ) ; :: thesis: K1 = K2

now :: thesis: for x being object holds
( ( 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 ) )

let x be object ; :: 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

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

end;

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

proof

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

end;

end;

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