let K, L be non empty ComplLattStr ; :: thesis: ( ComplLattStr(# the carrier of K,the L_join of K,the Compl of K #) = ComplLattStr(# the carrier of L,the L_join of L,the Compl of L #) & K is with_Top implies L is with_Top )
assume A1: ( ComplLattStr(# the carrier of K,the L_join of K,the Compl of K #) = ComplLattStr(# the carrier of L,the L_join of L,the Compl of L #) & 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 x' = x, y' = y as Element of K by A1;
x |_| (x ` ) = x' |_| (x' ` ) by A1, Th18
.= y' |_| (y' ` ) by A1, Def7
.= y |_| (y ` ) by A1, Th18 ;
hence x |_| (x ` ) = y |_| (y ` ) ; :: thesis: verum

end;

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