let K1, K2 be strict full SubRelStr of L; :: thesis:
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:

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

assume A4: x in the carrier of K1 ; :: thesis:
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:

end;

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

assume A5: x in the carrier of K2 ; :: thesis:
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:

end;