let S, T be non empty reflexive antisymmetric up-complete RelStr ; :: thesis: for x being Element of [:S,T:] st x is compact holds
( x `1 is compact & x `2 is compact )
let x be Element of [:S,T:]; :: thesis: ( x is compact implies ( x `1 is compact & x `2 is compact ) )
assume A1: x << x ; :: according to WAYBEL_3:def 2 :: thesis: ( x `1 is compact & x `2 is compact )
hence x `1 << x `1 by Th20; :: according to WAYBEL_3:def 2 :: thesis: x `2 is compact
thus x `2 << x `2 by A1, Th20; :: according to WAYBEL_3:def 2 :: thesis: verum