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
.= y |_| (y `) by A1, Th18 ;
hence x |_| (x `) = y |_| (y `) ; :: thesis: verum
end;
hence L is with_Top ; :: thesis: verum