let K, L be non empty ComplLLattStr ; :: thesis: ( ComplLLattStr(# the carrier of K,the L_join of K,the Compl of K #) = ComplLLattStr(# the carrier of L,the L_join of L,the Compl of L #) & K is with_Top implies L is with_Top )
assume that
A1: ComplLLattStr(# the carrier of K,the L_join of K,the Compl of K #) = ComplLLattStr(# the carrier of L,the L_join of L,the Compl of L #) and
A2: K is with_Top ; :: thesis: L is with_Top
for x, y being Element of L holds x |_| (x ` ) = y |_| (y ` )

proof

let x, y be Element of L; :: thesis: x |_| (x ` ) = y |_| (y ` )
reconsider x9 = x, y9 = y as Element of K by A1;
x |_| (x ` ) = x9 |_| (x9 ` ) by A1, Th18
.= y9 |_| (y9 ` ) by A2, Def7
.= y |_| (y ` ) by A1, Th18 ;
hence x |_| (x ` ) = y |_| (y ` ) ; :: thesis: verum

end;

hence L is with_Top by Def7; :: thesis: verum